diff --git a/keymaps/language-idris.json b/keymaps/language-idris.json
index 6d9f212..9274a4a 100644
--- a/keymaps/language-idris.json
+++ b/keymaps/language-idris.json
@@ -14,7 +14,20 @@
"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"
+ "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\"]": {
@@ -32,6 +45,19 @@
"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"
+ "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/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",