From edf88a5a6218b50a15b5056bf0a786a3a35f01ac Mon Sep 17 00:00:00 2001 From: Markus Klink Date: Tue, 22 Aug 2017 10:33:19 +0200 Subject: [PATCH 01/12] Move parser and logger to utils directory --- lib/idris-controller.coffee | 2 +- lib/idris-ide-mode.coffee | 4 ++-- lib/idris-model.coffee | 2 +- lib/{ => utils}/Logger.coffee | 0 lib/{ => utils}/parse.coffee | 3 +++ spec/parse-spec.coffee | 2 +- 6 files changed, 8 insertions(+), 5 deletions(-) rename lib/{ => utils}/Logger.coffee (100%) rename lib/{ => utils}/parse.coffee (92%) diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee index 3cda161..9551749 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' diff --git a/lib/idris-ide-mode.coffee b/lib/idris-ide-mode.coffee index 1d92102..0d547fa 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' 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 100% rename from lib/Logger.coffee rename to lib/utils/Logger.coffee 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/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)" From e3422ab52e35570c0c4097b1f496890f9b4f287c Mon Sep 17 00:00:00 2001 From: Markus Klink Date: Tue, 4 Sep 2018 13:59:06 +0200 Subject: [PATCH 02/12] import sexp-formatter from utils --- lib/utils/Logger.coffee | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/utils/Logger.coffee b/lib/utils/Logger.coffee index 87f09dc..1eab21f 100644 --- a/lib/utils/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" From 7f015f88e305f60edd723d0077a6c3f592f87524 Mon Sep 17 00:00:00 2001 From: Markus Klink Date: Tue, 4 Sep 2018 13:59:45 +0200 Subject: [PATCH 03/12] Pass tabLength from Atom Settings to ide-mode to steer indendation --- lib/idris-ide-mode.coffee | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/lib/idris-ide-mode.coffee b/lib/idris-ide-mode.coffee index 0d547fa..778c5c3 100644 --- a/lib/idris-ide-mode.coffee +++ b/lib/idris-ide-mode.coffee @@ -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 From c98aabdf019caea7e38e8d7b4298c1ce61b4bcbb Mon Sep 17 00:00:00 2001 From: Markus Klink Date: Tue, 4 Sep 2018 14:02:03 +0200 Subject: [PATCH 04/12] Prevent idris compiler crash when sending wrong make-with command --- lib/idris-controller.coffee | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee index 9551749..be68a7e 100644 --- a/lib/idris-controller.coffee +++ b/lib/idris-controller.coffee @@ -189,6 +189,7 @@ class IdrisController @saveFile editor uri = editor.getURI() word = Symbol.serializeWord editorHelper.getWordUnderCursor(editor) + @clearMessagePanel 'Idris: Searching type of ' + word + ' ...' successHandler = ({ responseType, msg }) => @@ -320,12 +321,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 }) => From db0f62a2d91f40c245943becfe5a5effdc60f6a6 Mon Sep 17 00:00:00 2001 From: Markus Klink Date: Thu, 6 Sep 2018 17:21:38 +0200 Subject: [PATCH 05/12] Fixes #206 --- lib/idris-controller.coffee | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee index be68a7e..51248ce 100644 --- a/lib/idris-controller.coffee +++ b/lib/idris-controller.coffee @@ -327,7 +327,7 @@ class IdrisController .filter ({ responseType }) -> responseType == 'return' .flatMap => @model.makeWith line + 1, word .subscribe successHandler, @displayErrors - else + else @clearMessagePanel "Idris: Illegal position to make a with view" # construct a lemma from a hole @@ -402,6 +402,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 From 27af5e0cc2f3b2897f3db547f05082f14fdd0e8d Mon Sep 17 00:00:00 2001 From: Markus Klink Date: Fri, 7 Sep 2018 13:06:18 +0200 Subject: [PATCH 06/12] Fixes #187 --- lib/utils/ipkg.coffee | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From 87bb683562fe9c5aa86ce55e51a043455e847edc Mon Sep 17 00:00:00 2001 From: Markus Klink Date: Fri, 7 Sep 2018 14:06:15 +0200 Subject: [PATCH 07/12] Prefix the function with a space The underlying bug is in the sexp-formatter which always treats strings starting with : as symbol. This breaks clauses like ":|:" since they are not being quoted This fixes #185 --- lib/idris-controller.coffee | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee index be68a7e..053b14d 100644 --- a/lib/idris-controller.coffee +++ b/lib/idris-controller.coffee @@ -238,11 +238,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() @@ -327,7 +329,7 @@ class IdrisController .filter ({ responseType }) -> responseType == 'return' .flatMap => @model.makeWith line + 1, word .subscribe successHandler, @displayErrors - else + else @clearMessagePanel "Idris: Illegal position to make a with view" # construct a lemma from a hole From fb86f021330370a07d00d1e22b06452e14a9b13e Mon Sep 17 00:00:00 2001 From: Markus Klink Date: Mon, 10 Sep 2018 10:11:04 +0200 Subject: [PATCH 08/12] Add DEVELOPMENT guide --- DEVELOPMENT.md | 65 ++++++++++++++++++++++++++++++++++++++++++++++++++ README.md | 7 +----- 2 files changed, 66 insertions(+), 6 deletions(-) create mode 100644 DEVELOPMENT.md 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 4846cb4..387fba6 100644 --- a/README.md +++ b/README.md @@ -53,9 +53,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) From 7075b2621e6344e9a52d5624bde008cca8b4d555 Mon Sep 17 00:00:00 2001 From: Markus Klink Date: Wed, 12 Sep 2018 10:47:07 +0200 Subject: [PATCH 09/12] Improve proof search When the result of the proof search returns an :ok message starting with a ?, display that the proof search was not succesful, otherwise insert the found proof. Fixes #199 --- lib/idris-controller.coffee | 28 ++++++++++++++++------------ 1 file changed, 16 insertions(+), 12 deletions(-) diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee index 5f18ea3..fe0626a 100644 --- a/lib/idris-controller.coffee +++ b/lib/idris-controller.coffee @@ -451,18 +451,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 From 76f8d9550d32e52c1fdde66669cec5e991959c0b Mon Sep 17 00:00:00 2001 From: Markus Klink Date: Wed, 12 Sep 2018 17:22:28 +0200 Subject: [PATCH 10/12] onsider Elaboration in infix grammar Infix grammar handles multiline cases like `plus`. however elaboration scripts know the terms `(x), `{x} and `{{x}} resulting in unclosed backticks which trip the grammar. This is an attempt to exclude these special cases in the handling of infix functions. --- grammars/language-idris.cson | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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' From 0fb35c9269b0ece6f0a3c0c14907751c6ae031f7 Mon Sep 17 00:00:00 2001 From: Niklas Larsson Date: Wed, 12 Sep 2018 21:29:33 +0200 Subject: [PATCH 11/12] Update version to 0.5.0 --- package.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/package.json b/package.json index 86d4096..d460ca8 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", From 979c24102cef614d9c8eccc8bbe9c34b830f22a1 Mon Sep 17 00:00:00 2001 From: Markus Klink Date: Wed, 19 Sep 2018 11:46:31 +0200 Subject: [PATCH 12/12] ESC will close information panel Anytime you press ESC in the main editor the information panel will be closed. Fixes #196 --- keymaps/language-idris.json | 6 ++++-- lib/idris-controller.coffee | 5 +++-- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/keymaps/language-idris.json b/keymaps/language-idris.json index 4771b41..d40ac67 100644 --- a/keymaps/language-idris.json +++ b/keymaps/language-idris.json @@ -11,7 +11,8 @@ "ctrl-alt-r": "language-idris:typecheck", "ctrl-alt-m": "language-idris:make-case", "ctrl-alt-p": "language-idris:add-proof-clause", - "ctrl-alt-b": "language-idris:browse-namespace" + "ctrl-alt-b": "language-idris:browse-namespace", + "escape": "language-idris:close-information-view" }, ".platform-darwin, atom-text-editor[data-grammar~=\"idris\"]": { @@ -26,6 +27,7 @@ "ctrl-cmd-r": "language-idris:typecheck", "ctrl-cmd-m": "language-idris:make-case", "ctrl-cmd-p": "language-idris:add-proof-clause", - "ctrl-cmd-b": "language-idris:browse-namespace" + "ctrl-cmd-b": "language-idris:browse-namespace", + "escape": "language-idris:close-information-view" } } diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee index fe0626a..26737cd 100644 --- a/lib/idris-controller.coffee +++ b/lib/idris-controller.coffee @@ -29,6 +29,7 @@ class IdrisController 'language-idris:apropos': @runCommand @apropos 'language-idris:add-proof-clause': @runCommand @doAddProofClause 'language-idris:browse-namespace': @runCommand @doBrowseNamespace + 'language-idris:close-information-view': @hideAndClearMessagePanel isIdrisFile: (uri) -> uri?.match? /\.idr$/ @@ -70,14 +71,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()