Merge branch 'master' into improve-keymap-defaults

Author: ulidtko

DEVELOPMENT.md

@@ -0,0 +1,65 @@
+# Development Guide
+
+## Getting started
+
+The easiest way is to get the source of the `language-idris` package via the `apm`-tooling:
+
+```bash
+apm dev language-idris
+```
+
+This will install the package in the folder `~/github/language-idris`. You will then be able to use the development version of `language-idris` by invoking atom from any directory containing some idris files using
+
+```bash
+atom -d .
+```
+
+## Development process
+
+Atom is basically a browser and when doing development it can be useful to open the dev console.
+
+<kbd>Alt</kbd>+<kbd>Cmd</kbd><kbd>i</kbd> opens the developer console on Mac OS X. This enables you to see console logging output and exceptions.
+
+You can edit the sourcecode in another atom window:
+
+```
+$~/github/language-idris> atom .
+```
+
+Anytime you want to restart your project with the latest changes, you can just reload the window using `Window: Reload`.
+
+## Code Structure
+
+```bash
+~/github/language-idris/lib (master %)$ tree
+.
+├── idris-controller.coffee
+├── idris-ide-mode.coffee
+├── idris-model.coffee
+├── language-idris.coffee
+├── utils
+│   ├── Logger.coffee
+│   ├── dom.coffee
+│   ├── editor.coffee
+│   ├── highlighter.coffee
+│   ├── ipkg.coffee
+│   ├── js.coffee
+│   ├── parse.coffee
+│   ├── sexp-formatter.coffee
+│   └── symbol.coffee
+└── views
+    ├── apropos-view.coffee
+    ├── holes-view.coffee
+    ├── information-view.coffee
+    ├── panel-view.coffee
+    └── repl-view.coffee
+```
+
+The best point to get started is to dig into `idris-controller.coffee`. Almost all defined commands talk to a spawned idris process using the [Idris IDE protocol](http://docs.idris-lang.org/en/latest/reference/ide-protocol.html). This protocol communicates with Idris via S-Exp Expressions. If you want to see this communication have a look at `utils/Logger.coffee`.
+
+In order to send a command to idris, you will probably need some information from the current editor context. There are plenty of examples in the code and a helper package in the `utils` section. Once you have a reply you will probably need to format it. This can be done via one of the `highlighters`. Again, this is something which occurs again and again in the code.
+
+
+## Specs
+
+There are (too) few tests defined in the spec directory. You can execute them using `Window: Run package specs`.

README.md

@@ -54,9 +54,4 @@ There is more information available in a in a [separate documentation](https://g
 
 ## Development
 
-To work on this plugin you need to clone it into your atom directory
-and rename the folder to `language-idris` or the package settings won't get picked up.
-Then you need an `apm install` from the `language-idris` folder to install the dependencies.
-
-Or you can execute `apm dev language-idris`. This will install the package in a separate directory and you need to start
-Atom in dev-mode to load the development packages (`atom -d your/folder`).
+see the [Development Guide](DEVELOPMENT.md)

grammars/language-idris.cson

@@ -106,7 +106,7 @@ patterns:
     }
     {
       name: 'keyword.operator.function.infix.idris'
-      begin: '`'
+      begin: '`(?![\{|\(])'
       beginCaptures:
         0:
           name: 'punctuation.definition.entity.idris'

keymaps/language-idris.json

@@ -14,6 +14,7 @@
     "ctrl-i t": "language-idris:type-of",
     "ctrl-i w": "language-idris:make-with",
     "ctrl-i enter": "language-idris:open-repl",
+    "escape": "language-idris:close-information-view"
 
     "ctrl-alt-a": "language-idris:legacy-keymap-notice",
     "ctrl-alt-b": "language-idris:legacy-keymap-notice",
@@ -44,6 +45,7 @@
     "cmd-i t": "language-idris:type-of",
     "cmd-i w": "language-idris:make-with",
     "cmd-i enter": "language-idris:open-repl",
+    "escape": "language-idris:close-information-view"
 
     "cmd-alt-a": "language-idris:legacy-keymap-notice",
     "cmd-alt-b": "language-idris:legacy-keymap-notice",

lib/idris-controller.coffee

@@ -2,7 +2,7 @@
   require 'atom-message-panel'
 InformationView = require './views/information-view'
 HolesView = require './views/holes-view'
-Logger = require './Logger'
+Logger = require './utils/Logger'
 IdrisModel = require './idris-model'
 Ipkg = require './utils/ipkg'
 Symbol = require './utils/symbol'
@@ -31,6 +31,7 @@ class IdrisController
     'language-idris:add-proof-clause': @runCommand @doAddProofClause
     'language-idris:browse-namespace': @runCommand @doBrowseNamespace
     'language-idris:legacy-keymap-notice': migrations.showKeymapDeprecationNotice
+    'language-idris:close-information-view': @hideAndClearMessagePanel
 
   isIdrisFile: (uri) ->
     uri?.match? /\.idr$/
@@ -72,14 +73,14 @@ class IdrisController
     @statusbar.destroy()
 
   # clear the message panel and optionally display a new title
-  clearMessagePanel: (title) ->
+  clearMessagePanel: (title) =>
     @messages.attach()
     @messages.show()
     @messages.clear()
     @messages.setTitle title, true if title?
 
   # hide the message panel
-  hideAndClearMessagePanel: () ->
+  hideAndClearMessagePanel: () =>
     @clearMessagePanel()
     @messages.hide()
 
@@ -191,6 +192,7 @@ class IdrisController
     @saveFile editor
     uri = editor.getURI()
     word = Symbol.serializeWord editorHelper.getWordUnderCursor(editor)
+
     @clearMessagePanel 'Idris: Searching type of <tt>' + word + '</tt> ...'
 
     successHandler = ({ responseType, msg }) =>
@@ -239,11 +241,13 @@ class IdrisController
     @saveFile editor
     uri = editor.getURI()
     line = editor.getLastCursor().getBufferRow()
-    word = editorHelper.getWordUnderCursor editor
+    # by adding a clause we make sure that the word is
+    # not treated as a symbol
+    word = ' ' + editorHelper.getWordUnderCursor editor
 
     @clearMessagePanel 'Idris: Add clause ...'
 
-    successHandler = ({ responseType, msg }) =>
+    successHandler =  ({ responseType, msg }) =>
       [clause] = @prefixLiterateClause msg
 
       @hideAndClearMessagePanel()
@@ -322,12 +326,14 @@ class IdrisController
         editor.moveToBeginningOfLine()
         editor.moveUp()
 
-
-    @model
-      .load uri
-      .filter ({ responseType }) -> responseType == 'return'
-      .flatMap => @model.makeWith line + 1, word
-      .subscribe successHandler, @displayErrors
+    if (word?.length)
+      @model
+        .load uri
+        .filter ({ responseType }) -> responseType == 'return'
+        .flatMap => @model.makeWith line + 1, word
+        .subscribe successHandler, @displayErrors
+    else
+      @clearMessagePanel "Idris: Illegal position to make a with view"
 
   # construct a lemma from a hole
   doMakeLemma: ({ target }) =>
@@ -401,6 +407,7 @@ class IdrisController
 
       editor.transact ->
         # Delete old line, insert the new case block
+        editor.moveToBeginningOfLine()
         editor.deleteLine()
         editor.insertText clause
         # And move the cursor to the beginning of
@@ -447,18 +454,22 @@ class IdrisController
       [res] = msg
 
       @hideAndClearMessagePanel()
-
-      editor.transact ->
-        # Move the cursor to the beginning of the word
-        editor.moveToBeginningOfWord()
-        # Because the ? in the Holes isn't part of
-        # the word, we move left once, and then select two
-        # words
-        editor.moveLeft()
-        editor.selectToEndOfWord()
-        editor.selectToEndOfWord()
-        # And then replace the replacement with the guess..
-        editor.insertText res
+      console.log res
+      if (res.startsWith("?"))
+        # proof search returned a new hole
+        @clearMessagePanel 'Idris: Searching proof was not successful.'
+      else
+        editor.transact ->
+          # Move the cursor to the beginning of the word
+          editor.moveToBeginningOfWord()
+          # Because the ? in the Holes isn't part of
+          # the word, we move left once, and then select two
+          # words
+          editor.moveLeft()
+          editor.selectToEndOfWord()
+          editor.selectToEndOfWord()
+          # And then replace the replacement with the guess..
+          editor.insertText res
 
     @model
       .load uri

lib/idris-ide-mode.coffee

@@ -1,6 +1,6 @@
-Logger = require './Logger'
+Logger = require './utils/Logger'
 sexpFormatter = require './utils/sexp-formatter'
-parse = require './parse'
+parse = require './utils/parse'
 { EventEmitter } = require 'events'
 { spawn } = require 'child_process'
 
@@ -26,8 +26,12 @@ class IdrisIdeMode extends EventEmitter
         else
           []
 
+      tabLength = atom.config.get('editor.tabLength', scope: ['source.idris'])
+      configParams = ['--ide-mode', '--indent-with=' + tabLength,
+                      '--indent-clause=' + tabLength]
+
       parameters =
-        ['--ide-mode'].concat pkgs, options
+        configParams.concat pkgs, options
 
       options =
         if compilerOptions.src

lib/idris-model.coffee

@@ -1,5 +1,5 @@
 IdrisIdeMode = require './idris-ide-mode'
-Logger = require './Logger'
+Logger = require './utils/Logger'
 Rx = require 'rx-lite'
 JS = require './utils/js'
 path = require 'path'

lib/Logger.coffee renamed to lib/utils/Logger.coffee

@@ -1,5 +1,5 @@
 fs = require 'fs'
-sexpFormatter = require './utils/sexp-formatter'
+sexpFormatter = require './sexp-formatter'
 
 class Logger
   logFile: "log.log"

lib/utils/ipkg.coffee

@@ -4,7 +4,7 @@ Rx = require 'rx-lite'
 
 optionsRegexp = /opts\s*=\s*\"([^\"]*)\"/
 sourcedirRegexp = /sourcedir\s*=\s*([a-zA-Z/0-9.]+)/
-pkgsRegexp = /pkgs\s*=\s*([a-zA-Z/0-9., ]+)/
+pkgsRegexp = /pkgs\s*=\s*(([a-zA-Z/0-9., ]+\s{0,1})*)/
 
 # Find all ipkg-files in a directory and returns
 # an observable of an array of files

lib/parse.coffee renamed to lib/utils/parse.coffee

@@ -1,6 +1,9 @@
 { parse, text, lang } = require 'bennu'
 { stream } = require 'nu-stream'
 
+# this module defines the parse required to deal with S-Expressions
+# as used for the communication with the Idris IDE
+
 streamToString = (s) -> stream.toArray(s).join ''
 
 # bool