Better default keymap prefix Ctrl-Alt → Ctrl-i

README.md

@@ -6,29 +6,30 @@ A work-in-progress Idris Mode for Atom.
 
 It supports:
 
- - Typechecking (ctrl-alt-r)
+ - Typechecking (<kbd>ctrl-i</kbd> <kbd>r</kbd>)
    - compiles the file and reports errors
- - Case-splitting (ctrl-alt-c)
+ - Case-splitting (<kbd>ctrl-i</kbd> <kbd>c</kbd>)
    - split a variable which can be pattern matched
- - Clause-adding (ctrl-alt-a)
+ - Clause-adding (<kbd>ctrl-i</kbd> <kbd>a</kbd>)
    - add a clause to a function
- - Proof-search (ctrl-alt-s)
+ - Proof-search (<kbd>ctrl-i</kbd> <kbd>s</kbd>)
    - search for a proof of a hole
- - Showing the types of a variable (ctrl-alt-t)
+ - Showing the types of a variable (<kbd>ctrl-i</kbd> <kbd>t</kbd>)
    - 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 (<kbd>ctrl-i</kbd> <kbd>d</kbd>)
+ - Print definition of data type, function, interface (<kbd>ctrl-i</kbd> <kbd>f</kbd>)
+ - make-with (<kbd>ctrl-i</kbd> <kbd>w</kbd>)
    - add further variables on the left hand side of a function
- - make-case (ctrl-alt-m)
- - make-lemma (ctrl-alt-l)
+ - make-case (<kbd>ctrl-i</kbd> <kbd>m</kbd>)
+ - make-lemma (<kbd>ctrl-i</kbd> <kbd>l</kbd>)
    - lift a hole into a function context
- - Add proof case (ctrl-alt-p)
+ - Add proof case (<kbd>ctrl-i</kbd> <kbd>p</kbd>)
    - 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 (<kbd>ctrl-i</kbd> <kbd>b</kbd>)
    - select the name of a namespace beforehand
- - Showing holes
+ - Showing holes (<kbd>ctrl-i</kbd> <kbd>o</kbd>)
  - ipkg highlighting
- - REPL (ctrl-alt-enter)
+ - REPL (<kbd>ctrl-i</kbd> <kbd>enter</kbd>)
  - Apropos view
 
 ## Usage

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.
 

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"
   }
 }

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$/

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 <kbd>ctrl-i</kbd><kbd>r</kbd>,
+                 <kbd>ctrl-i</kbd><kbd>t</kbd>,
+                 <kbd>ctrl-i</kbd><kbd>c</kbd> shortcuts
+      instead of <kbd>ctrl-alt-r</kbd>,
+                 <kbd>ctrl-alt-t</kbd>,
+                 <kbd>ctrl-alt-c</kbd>... etc.
+
+      As usual, you can learn Idris shortcuts in Command Palette:
+      <kbd>ctrl-shift-p</kbd> or <kbd>cmd-shift-p</kbd>, 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."
+            )
+        }
+      ]
+    )

menus/language-idris.cson

@@ -48,6 +48,10 @@
           'label': 'Docs for'
           'command': 'language-idris:docs-for'
         }
+        {
+          'label': 'Show definition'
+          'command': 'language-idris:print-definition'
+        }
       ]
     }
   ]

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",