diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md new file mode 100644 index 0000000..be29f99 --- /dev/null +++ b/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. + +Alt+Cmdi 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`. diff --git a/README.md b/README.md index 9e55c09..eb84ab9 100644 --- a/README.md +++ b/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) diff --git a/grammars/language-idris.cson b/grammars/language-idris.cson index 320bd39..34562e6 100644 --- a/grammars/language-idris.cson +++ b/grammars/language-idris.cson @@ -106,7 +106,7 @@ patterns: } { name: 'keyword.operator.function.infix.idris' - begin: '`' + begin: '`(?![\{|\(])' beginCaptures: 0: name: 'punctuation.definition.entity.idris' diff --git a/keymaps/language-idris.json b/keymaps/language-idris.json index 9c87fd5..e274874 100644 --- a/keymaps/language-idris.json +++ b/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", diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee index 42fbec6..c638a5a 100644 --- a/lib/idris-controller.coffee +++ b/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 ' + word + ' ...' 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 diff --git a/lib/idris-ide-mode.coffee b/lib/idris-ide-mode.coffee index 1d92102..778c5c3 100644 --- a/lib/idris-ide-mode.coffee +++ b/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 diff --git a/lib/idris-model.coffee b/lib/idris-model.coffee index fe81f56..1baf160 100644 --- a/lib/idris-model.coffee +++ b/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' diff --git a/lib/Logger.coffee b/lib/utils/Logger.coffee similarity index 89% rename from lib/Logger.coffee rename to lib/utils/Logger.coffee index 87f09dc..1eab21f 100644 --- a/lib/Logger.coffee +++ b/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" diff --git a/lib/utils/ipkg.coffee b/lib/utils/ipkg.coffee index 8cce9fc..8d28571 100644 --- a/lib/utils/ipkg.coffee +++ b/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 diff --git a/lib/parse.coffee b/lib/utils/parse.coffee similarity index 92% rename from lib/parse.coffee rename to lib/utils/parse.coffee index 1e0d9bf..eb911f5 100644 --- a/lib/parse.coffee +++ b/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 diff --git a/package.json b/package.json index eb9e1d1..f889c25 100644 --- a/package.json +++ b/package.json @@ -1,7 +1,7 @@ { "name": "language-idris", "main": "./lib/language-idris", - "version": "0.4.10", + "version": "0.5.0", "private": true, "description": "A plugin for developing with Idris", "repository": "https://github.com/idris-hackers/atom-language-idris", diff --git a/spec/parse-spec.coffee b/spec/parse-spec.coffee index 3af1194..226132f 100644 --- a/spec/parse-spec.coffee +++ b/spec/parse-spec.coffee @@ -1,5 +1,5 @@ sexpFormatter = require '../lib/utils/sexp-formatter' -parse = require '../lib/parse' +parse = require '../lib/utils/parse' runP = require('bennu').parse.run test1 = "(:protocol-version 1 0)"