diff --git a/README.md b/README.md index 387fba6..eb84ab9 100644 --- a/README.md +++ b/README.md @@ -6,29 +6,30 @@ A work-in-progress Idris Mode for Atom. It supports: - - Typechecking (ctrl-alt-r) + - Typechecking (ctrl-i r) - compiles the file and reports errors - - Case-splitting (ctrl-alt-c) + - Case-splitting (ctrl-i c) - split a variable which can be pattern matched - - Clause-adding (ctrl-alt-a) + - Clause-adding (ctrl-i a) - add a clause to a function - - Proof-search (ctrl-alt-s) + - Proof-search (ctrl-i s) - search for a proof of a hole - - Showing the types of a variable (ctrl-alt-t) + - Showing the types of a variable (ctrl-i t) - show the type of a hole - - Show the doc for a function (ctrl-alt-d) - - make-with (ctrl-alt-w) + - Show the doc for a function or interface (ctrl-i d) + - Print definition of data type, function, interface (ctrl-i f) + - make-with (ctrl-i w) - add further variables on the left hand side of a function - - make-case (ctrl-alt-m) - - make-lemma (ctrl-alt-l) + - make-case (ctrl-i m) + - make-lemma (ctrl-i l) - lift a hole into a function context - - Add proof case (ctrl-alt-p) + - Add proof case (ctrl-i p) - alternate version of clause adding when trying to proof a type. http://docs.idris-lang.org/en/latest/reference/misc.html#match-application - - Browse namespace (ctrl-alt-b) + - Browse namespace (ctrl-i b) - select the name of a namespace beforehand - - Showing holes + - Showing holes (ctrl-i o) - ipkg highlighting - - REPL (ctrl-alt-enter) + - REPL (ctrl-i enter) - Apropos view ## Usage diff --git a/documentation/tutorial.md b/documentation/tutorial.md index 0be5983..f6daf8f 100644 --- a/documentation/tutorial.md +++ b/documentation/tutorial.md @@ -31,27 +31,27 @@ mul (S k) y = add y (mul k y) ### Typecheck -Open the command palette (`ctrl-shift-p` on Win/Linux) and select `Language Idris: Typecheck`. (or use `ctrl-alt-r`) +Open the command palette (`ctrl-shift-p` on Win/Linux) and select `Language Idris: Typecheck`. (or use `ctrl-i r`) ### Type info -Select an instance of the `add` function in your code and press `ctrl-alt-t` or use the command palette (`ctrl-shift-p` on Win/Linux) and search for "Language Idris: Type Of". A panel should open at the bottom of your window showing you the type of the `add` function, `Ops.add : Nat -> Nat -> Nat`. +Select an instance of the `add` function in your code and press `ctrl-i t` or use the command palette (`ctrl-shift-p` on Win/Linux) and search for "Language Idris: Type Of". A panel should open at the bottom of your window showing you the type of the `add` function, `Ops.add : Nat -> Nat -> Nat`. Now try the same thing with the `mul` function. ### Show documentation -Another useful command is triggered by selecting a word and pressing `ctrl-alt-d` (or "Language Idris: Docs for" from the command palette). You can try it on `add`, `mul` or `Nat` for instance. +Another useful command is triggered by selecting a word and pressing `ctrl-i d` (or "Language Idris: Docs for" from the command palette). You can try it on `add`, `mul` or `Nat` for instance. ### REPL -You can create a REPL window by pressing `ctrl-alt-enter`. Enter REPL commands at the top, just as if you were using the REPL command line interface. +You can create a REPL window by pressing `ctrl-i enter`. Enter REPL commands at the top, just as if you were using the REPL command line interface. -### Idris command line options and library package dependencies +### Idris command line options and library package dependencies -Sometimes you may have dependendencies on Idris packages, for instance Lightyear for parsing or Pruvioj for advanced theorem proving. -In Atom you can specify these dependencies using the project model, which simply means using Open Folder rather than Open File -from the File menu. Atom will look for a .ipkg file in the folder and load any dependencies listed. More details are described in -[Working with ipkg files](https://github.com/idris-hackers/atom-language-idris/blob/master/documentation/ipkg.md). +Sometimes you may have dependendencies on Idris packages, for instance Lightyear for parsing or Pruvioj for advanced theorem proving. +In Atom you can specify these dependencies using the project model, which simply means using Open Folder rather than Open File +from the File menu. Atom will look for a .ipkg file in the folder and load any dependencies listed. More details are described in +[Working with ipkg files](https://github.com/idris-hackers/atom-language-idris/blob/master/documentation/ipkg.md). ## Interactive proofs using Idris and Atom @@ -66,7 +66,7 @@ module Main plusAssoc : (l, c, r : Nat) -> l `plus` (c `plus` r) = (l `plus` c) `plus` r ``` -Load the file into Idris by typechecking it by pressing `ctrl-alt-r`. Then press `ctrl-shift-p` and type "Language Idris: Holes". +Load the file into Idris by typechecking it by pressing `ctrl-i r`. Then press `ctrl-shift-p` and type "Language Idris: Holes". At the bottom of your window should open a small panel with all holes you'll have to prove. Here it should just show: @@ -81,7 +81,7 @@ Main.plusAssoc : plus l (plus c r) = plus (plus l c) r where `l : Nat, c : Nat, r : Nat` are variables you can use to prove `Main.plusAssoc : plus l (plus c r) = plus (plus l c) r`. -If you put your cursor over `plusAssoc` in the `proving.idr` file and execute the command "Language Idris: Add Clause" (`ctrl-alt-a`) a line wil be inserted by atom at the bottom of your file. +If you put your cursor over `plusAssoc` in the `proving.idr` file and execute the command "Language Idris: Add Clause" (`ctrl-i a`) a line wil be inserted by atom at the bottom of your file. Your file should now look like this: ```idris @@ -91,7 +91,7 @@ plusAssoc : (l, c, r : Nat) -> l `plus` (c `plus` r) = (l `plus` c) `plus` r plusAssoc l c r = ?plusAssoc_rhs ``` -If you select the `l` in `plusAssoc l c r = ?plusAssoc_rhs` and press `ctrl-alt-c` ("Language Idris: Case Split") it splits the `Nat` at `l` +If you select the `l` in `plusAssoc l c r = ?plusAssoc_rhs` and press `ctrl-i c` ("Language Idris: Case Split") it splits the `Nat` at `l` into it's two cases `Z` (zero) and `(S k)` (the successor of `k`). Rename `k` to `l` as we had it before, to show that it is the left value. diff --git a/keymaps/language-idris.json b/keymaps/language-idris.json index d40ac67..9274a4a 100644 --- a/keymaps/language-idris.json +++ b/keymaps/language-idris.json @@ -1,33 +1,63 @@ { "atom-text-editor[data-grammar~=\"idris\"]": { - "ctrl-alt-c": "language-idris:case-split", - "ctrl-alt-t": "language-idris:type-of", - "ctrl-alt-a": "language-idris:add-clause", - "ctrl-alt-s": "language-idris:proof-search", - "ctrl-alt-d": "language-idris:docs-for", - "ctrl-alt-enter": "language-idris:open-repl", - "ctrl-alt-w": "language-idris:make-with", - "ctrl-alt-l": "language-idris:make-lemma", - "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", - "escape": "language-idris:close-information-view" + "ctrl-i a": "language-idris:add-clause", + "ctrl-i b": "language-idris:browse-namespace", + "ctrl-i c": "language-idris:case-split", + "ctrl-i d": "language-idris:docs-for", + "ctrl-i f": "language-idris:print-definition", + "ctrl-i l": "language-idris:make-lemma", + "ctrl-i m": "language-idris:make-case", + "ctrl-i o": "language-idris:holes", + "ctrl-i p": "language-idris:add-proof-clause", + "ctrl-i r": "language-idris:typecheck", + "ctrl-i s": "language-idris:proof-search", + "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", + "ctrl-alt-c": "language-idris:legacy-keymap-notice", + "ctrl-alt-d": "language-idris:legacy-keymap-notice", + "ctrl-alt-l": "language-idris:legacy-keymap-notice", + "ctrl-alt-m": "language-idris:legacy-keymap-notice", + "ctrl-alt-p": "language-idris:legacy-keymap-notice", + "ctrl-alt-r": "language-idris:legacy-keymap-notice", + "ctrl-alt-s": "language-idris:legacy-keymap-notice", + "ctrl-alt-t": "language-idris:legacy-keymap-notice", + "ctrl-alt-w": "language-idris:legacy-keymap-notice", + "ctrl-alt-enter": "language-idris:legacy-keymap-notice" }, - ".platform-darwin, atom-text-editor[data-grammar~=\"idris\"]": { - "ctrl-cmd-c": "language-idris:case-split", - "ctrl-cmd-t": "language-idris:type-of", - "ctrl-cmd-a": "language-idris:add-clause", - "ctrl-cmd-s": "language-idris:proof-search", - "ctrl-cmd-d": "language-idris:docs-for", - "ctrl-cmd-enter": "language-idris:open-repl", - "ctrl-cmd-w": "language-idris:make-with", - "ctrl-cmd-l": "language-idris:make-lemma", - "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", - "escape": "language-idris:close-information-view" + ".platform-darwin atom-text-editor[data-grammar~=\"idris\"]": { + "cmd-i a": "language-idris:add-clause", + "cmd-i b": "language-idris:browse-namespace", + "cmd-i c": "language-idris:case-split", + "cmd-i d": "language-idris:docs-for", + "cmd-i f": "language-idris:print-definition", + "cmd-i l": "language-idris:make-lemma", + "cmd-i m": "language-idris:make-case", + "cmd-i o": "language-idris:holes", + "cmd-i p": "language-idris:add-proof-clause", + "cmd-i r": "language-idris:typecheck", + "cmd-i s": "language-idris:proof-search", + "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", + "cmd-alt-c": "language-idris:legacy-keymap-notice", + "cmd-alt-d": "language-idris:legacy-keymap-notice", + "cmd-alt-l": "language-idris:legacy-keymap-notice", + "cmd-alt-m": "language-idris:legacy-keymap-notice", + "cmd-alt-p": "language-idris:legacy-keymap-notice", + "cmd-alt-r": "language-idris:legacy-keymap-notice", + "cmd-alt-s": "language-idris:legacy-keymap-notice", + "cmd-alt-t": "language-idris:legacy-keymap-notice", + "cmd-alt-w": "language-idris:legacy-keymap-notice", + "cmd-alt-enter": "language-idris:legacy-keymap-notice" } } diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee index 26737cd..7084fcc 100644 --- a/lib/idris-controller.coffee +++ b/lib/idris-controller.coffee @@ -8,6 +8,7 @@ Ipkg = require './utils/ipkg' Symbol = require './utils/symbol' editorHelper = require './utils/editor' highlighter = require './utils/highlighter' +migrations = require './migrations' class IdrisController errorMarkers: [] @@ -30,6 +31,7 @@ class IdrisController 'language-idris:add-proof-clause': @runCommand @doAddProofClause 'language-idris:browse-namespace': @runCommand @doBrowseNamespace 'language-idris:close-information-view': @hideAndClearMessagePanel + 'language-idris:legacy-keymap-notice': migrations.showKeymapDeprecationNotice isIdrisFile: (uri) -> uri?.match? /\.idr$/ diff --git a/lib/migrations.coffee b/lib/migrations.coffee new file mode 100644 index 0000000..71bdbd0 --- /dev/null +++ b/lib/migrations.coffee @@ -0,0 +1,81 @@ +# +# Throw out this module as soon as it becomes a maintenance burden, or +# sufficient stabilization time has passed for the new keymap. +# + +CSON = require 'cson-parser' + +formatLegacyKeymap = () -> + legacyKeymap = + "atom-text-editor[data-grammar~=\"idris\"]": + "ctrl-alt-a": "language-idris:add-clause" + "ctrl-alt-b": "language-idris:browse-namespace" + "ctrl-alt-c": "language-idris:case-split" + "ctrl-alt-d": "language-idris:docs-for" + "ctrl-alt-l": "language-idris:make-lemma" + "ctrl-alt-m": "language-idris:make-case" + "ctrl-alt-p": "language-idris:add-proof-clause" + "ctrl-alt-r": "language-idris:typecheck" + "ctrl-alt-s": "language-idris:proof-search" + "ctrl-alt-t": "language-idris:type-of" + "ctrl-alt-w": "language-idris:make-with" + "ctrl-alt-enter": "language-idris:open-repl" + ".platform-darwin atom-text-editor[data-grammar~=\"idris\"]": + "ctrl-cmd-a": "language-idris:add-clause" + "ctrl-cmd-b": "language-idris:browse-namespace" + "ctrl-cmd-c": "language-idris:case-split" + "ctrl-cmd-d": "language-idris:docs-for" + "ctrl-cmd-l": "language-idris:make-lemma" + "ctrl-cmd-m": "language-idris:make-case" + "ctrl-cmd-p": "language-idris:add-proof-clause" + "ctrl-cmd-r": "language-idris:typecheck" + "ctrl-cmd-s": "language-idris:proof-search" + "ctrl-cmd-t": "language-idris:type-of" + "ctrl-cmd-w": "language-idris:make-with" + "ctrl-cmd-enter": "language-idris:open-repl" + + keymapExtension = atom.keymaps.getUserKeymapPath().split('.').pop() + if keymapExtension == 'cson' + return CSON.stringify(legacyKeymap, null, 2) + if keymapExtension == 'json' + return JSON.stringify(legacyKeymap, null, 2) + + +module.exports = + showKeymapDeprecationNotice: -> + detailMd = """ + Please use ctrl-ir, + ctrl-it, + ctrl-ic shortcuts + instead of ctrl-alt-r, + ctrl-alt-t, + ctrl-alt-c... etc. + + As usual, you can learn Idris shortcuts in Command Palette: + ctrl-shift-p or cmd-shift-p, then type `Idris`. + + --- + + To get back the old `ctrl-alt` bindings *(not recommended)*, + click the "Edit keymap" button below, and paste. + """ + + popup = atom.notifications.addInfo("Default Idris keymap has been changed.", + dismissable: true + description: detailMd + buttons: [ + { text: "Dismiss", onDidClick: () -> popup.dismiss() } + { + text: "Edit keymap" + className: 'btn btn-warning icon icon-clippy copy-icon' + onDidClick: () -> + atom.clipboard.write(formatLegacyKeymap()) + atom.commands.dispatch(atom.views.getView(atom.workspace), + 'application:open-your-keymap') + popup.dismiss() + atom.notifications.addSuccess("Copied to clipboard", + description: "The old `ctrl-alt` Idris keymap can be pasted now." + ) + } + ] + ) diff --git a/menus/language-idris.cson b/menus/language-idris.cson index e51c32d..1ea4941 100644 --- a/menus/language-idris.cson +++ b/menus/language-idris.cson @@ -48,6 +48,10 @@ 'label': 'Docs for' 'command': 'language-idris:docs-for' } + { + 'label': 'Show definition' + 'command': 'language-idris:print-definition' + } ] } ] diff --git a/package.json b/package.json index d460ca8..f889c25 100644 --- a/package.json +++ b/package.json @@ -42,6 +42,7 @@ "dependencies": { "atom-message-panel": "^1.3.0", "bennu": "17.3.0", + "cson-parser": "^1.0.9", "nu-stream": "3.3.1", "rx-lite": "4.0.0", "@cycle/core": "3.1.0",