diff options
| author | David Aspinall | 2008-01-24 19:22:49 +0000 |
|---|---|---|
| committer | David Aspinall | 2008-01-24 19:22:49 +0000 |
| commit | 2fc3aa396f5f211f4c8e0e9dd55a099d63df58e3 (patch) | |
| tree | fcf35b191062e2c272703321f95d1194c19d17a1 | |
| parent | c4d8fac6c6821ecbe384ef3181eb129d54c6c8e3 (diff) | |
Add key binding for ML {* *} and fix longsuper, longsub
| -rw-r--r-- | isar/isar.el | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/isar/isar.el b/isar/isar.el index a3d2629f..f1efa6a0 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -129,6 +129,8 @@ See -k option for Isabelle interface script." proof-context-command "print_context" proof-info-command "welcome" proof-kill-goal-command "ProofGeneral.kill_proof" +;; da: TODO: we should set this from our own setting really, not suggest +;; people customize prover-confi ; proof-find-theorems-command "find_theorems %s" ;; minibuffer proof-find-theorems-command 'isar-find-theorems-minibuffer ;; equivalent ; proof-find-theorems-command 'isar-find-theorems-form ;; search form @@ -479,11 +481,12 @@ proof-shell-retract-files-regexp." (proof-defshortcut isar-local "\\<^loc>%p" [(control c)]) (proof-defshortcut isar-super "\\<^sup>%p" [(control u)]) (proof-defshortcut isar-sub "\\<^sub>%p" [(control l)]) -(proof-defshortcut isar-longsuper "\\<^bsup>%p\\<^esup>" [u]) -(proof-defshortcut isar-longsub "\\<^bsub>%p\\<^esub>" [l]) +(proof-defshortcut isar-longsuper "\\<^bsup>%p\\<^esup>" [?u]) +(proof-defshortcut isar-longsub "\\<^bsub>%p\\<^esub>" [?l]) (proof-defshortcut isar-idsub "\\<^isub>%p" [(control i)]) (proof-defshortcut isar-raw "\\<^raw:%p>" [(control r)]) (proof-defshortcut isar-antiquote "@{text \"%p\"}" [(control a)]) +(proof-defshortcut isar-ml "ML {* %p *}" [(control x)]) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |