diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | coq/coq.el | 34 | ||||
| -rw-r--r-- | generic/proof-config.el | 5 | ||||
| -rw-r--r-- | generic/proof-script.el | 11 | ||||
| -rw-r--r-- | generic/proof-syntax.el | 48 | ||||
| -rw-r--r-- | generic/proof.el | 22 | ||||
| -rw-r--r-- | isa/Example.ML | 2 | ||||
| -rw-r--r-- | lego/example.l | 1 | ||||
| -rw-r--r-- | lego/lego.el | 21 | ||||
| -rw-r--r-- | plastic/plastic.el | 33 |
10 files changed, 110 insertions, 71 deletions
@@ -9,6 +9,10 @@ Specific menus added for Coq, Isabelle. +*** Proof assistant specific keymap added + + Keybindings for proof assistant now begin with "C-c a". + *** Improved behaviour of electric terminator *** Efficiency improvement in parsing @@ -283,18 +283,6 @@ ;; Commands specific to coq ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun coq-Intros () - "Shortcut for Intros. -This is specific to coq-mode." - (interactive) - (insert "Intros ")) - -(defun coq-Apply () - "Shortcut for Apply -This is specific to coq-mode." - (interactive) - (insert "Apply ")) - (defun coq-SearchIsos () "Search a term whose type is isomorphic to given type This is specific to coq-mode." @@ -305,11 +293,6 @@ This is specific to coq-mode." (proof-shell-invisible-command (concat "SearchIsos " cmd proof-terminal-string)))) -(defun coq-begin-Section () - "begins a Coq section." - (interactive) - (insert "Section ")) - (defun coq-end-Section () "Ends a Coq section." (interactive) @@ -335,6 +318,15 @@ This is specific to coq-mode." (l (string-match ".v" n))) (compile (concat "make " (substring n 0 l) ".vo")))) +(proof-defshortcut coq-Intros "Intros " ?i) +(proof-defshortcut coq-Apply "Apply " ?a) +(proof-defshortcut coq-begin-Section "Section " ?s) + +(define-key proof-assistant-keymap ?e 'coq-end-Section) +(define-key proof-assistant-keymap ?m 'coq-Compile) +(define-key proof-assistant-keymap ?o 'coq-SearchIsos) + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Indentation ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -472,14 +464,6 @@ This is specific to coq-mode." (proof-config-done) -;; Coq-specific key mappings - - (define-key (current-local-map) [(control c) ?I] 'coq-Intros) - (define-key (current-local-map) [(control c) ?a] 'coq-Apply) - (define-key (current-local-map) [(control c) ?s] 'coq-begin-Section) - (define-key (current-local-map) [(control c) ?e] 'coq-end-Section) - (define-key (current-local-map) [(control c) (control m)] 'coq-Compile) - ;; outline (make-local-variable 'outline-regexp) diff --git a/generic/proof-config.el b/generic/proof-config.el index dc39cc62..e25d8c96 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -689,6 +689,11 @@ of `easy-menu-define' for more details." :type 'sexp :group 'prover-config) +(defcustom proof-assistant-keymap (make-keymap "proof-assistant-keymap") + "Proof assistant keymap, defined under prefix C-c a." + :type 'sexp + :group 'prover-config) + diff --git a/generic/proof-script.el b/generic/proof-script.el index 933bf1df..3481c4aa 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2267,10 +2267,12 @@ This is intended as a value for proof-activate-scripting-hook" "Proof General buffer menu.") ;; Make the togglers used in options menu below -(fset 'proof-dont-switch-windows-toggle - (proof-customize-toggle proof-dont-switch-windows)) -(fset 'proof-delete-empty-windows-toggle - (proof-customize-toggle proof-delete-empty-windows)) +;(fset 'proof-dont-switch-windows-toggle +; (proof-customize-toggle proof-dont-switch-windows)) +;(fset 'proof-delete-empty-windows-toggle +; (proof-customize-toggle proof-delete-empty-windows)) +(proof-deftoggle proof-dont-switch-windows) +(proof-deftoggle proof-delete-empty-windows) (fset 'proof-multiple-frames-toggle (proof-customize-toggle proof-multiple-frames-enable)) (fset 'proof-output-fontify-toggle @@ -2484,6 +2486,7 @@ Otherwise just do proof-restart-buffers to delete some spans from memory." ;; (let ((map proof-mode-map)) ; proof-mode-map comes from define-derived-mode above +(define-key map [(control c) a] proof-assistant-keymap) (define-key map [(control c) (control a)] 'proof-goto-command-start) (define-key map [(control c) (control b)] 'proof-process-buffer) ; C-c C-c is proof-interrupt-process in universal-keys diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index 703e2774..badf56b3 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -178,4 +178,52 @@ understand ~, for example." string)) +;; +;; Functions for inserting text into buffer. +;; +;; Added for version 3.2 to provide more prover specific shortcuts. +;; + +; Taken from Isamode +; +; %l - insert the value of isa-logic-name +; %s - insert the value returned by isa-current-subgoal + +(defun proof-insert (text) + "Insert TEXT into the current buffer. +TEXT may include these special characters: + %p - place the point here after input +Any other %-prefixed character inserts itself." + ; would be quite nice to have this function: + ;(isa-delete-pending-input) + (let ((i 0) pos acc) + (while (< i (length text)) + (let ((ch (elt text i))) + (if (not (eq ch ?%)) + (setq acc (concat acc (char-to-string ch))) + (setq i (1+ i)) + (setq ch (elt text i)) + (cond ;((eq ch ?l) + ; (setq acc (concat acc isa-logic-name))) + ;((eq ch ?s) + ; (setq acc + ; (concat acc + ; (int-to-string + ; (if (boundp 'isa-denoted-subgoal) + ; isa-denoted-subgoal + ; 1))))) + ;((eq ch ?n) + ; (if acc (insert acc)) + ; (setq acc nil) + ; (comint-send-input)) + ((eq ch ?p) + (if acc (insert acc)) + (setq acc nil) + (setq pos (point))) + (t (setq acc (concat acc (char-to-string ch))))))) + (setq i (1+ i))) + (if acc (insert acc)) + (if pos (goto-char pos)))) + + (provide 'proof-syntax) diff --git a/generic/proof.el b/generic/proof.el index ab51aa1e..102a8727 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -196,16 +196,32 @@ It was constructed with the macro proof-customize-toggle.") ;; FIXME: combine this with above, and remove messing calls in ;; proof-script. -;; FIXME: rather broken wrt to ARG. (defmacro proof-deftoggle (var) - "Define a function VAR-toggle to be a toggler for variable VAR. -See proof-customize-toggle." + "Define a function VAR-toggle for toggling a boolean customize setting VAR. +The toggle function uses customize-set-variable to change the variable." `(defun ,(intern (concat (symbol-name var) "-toggle")) (arg) + ,(concat "Toggle " (symbol-name var) ". With ARG, turn on iff ARG>0. +This function simply uses customize-set-variable to set the variable. +It was constructed with the macro proof-deftoggle.") (interactive "P") (customize-set-variable (quote ,var) (if (null arg) (not ,var) (> (prefix-numeric-value arg) 0))))) + +(defmacro proof-defshortcut (fn string &optional key) + "Define shortcut function FN to insert STRING, optional keydef KEY. +This is intended for defining proof assistant specific functions. +STRING is inserted using `proof-insert', which see. +KEY is added onto proof-assistant map." + (if key + (eval + `(define-key proof-assistant-keymap ,key (quote ,fn)))) + `(defun ,fn () + "Shortcut command to insert a string." + (interactive) + (proof-insert ,string))) + (defun proof-try-require (symbol) "Try requiring SYMBOL. No error if the file for SYMBOL isn't found." diff --git a/isa/Example.ML b/isa/Example.ML index 929c7ad8..bf5ee3f0 100644 --- a/isa/Example.ML +++ b/isa/Example.ML @@ -11,3 +11,5 @@ by (rtac conjI 1); by (assume_tac 1); by (assume_tac 1); qed "and_comms"; + +Goal "P(x) --> Q(x)"; diff --git a/lego/example.l b/lego/example.l index 535d5712..525db25b 100644 --- a/lego/example.l +++ b/lego/example.l @@ -5,7 +5,6 @@ *) Module example Import lib_logic; - Goal {A,B:Prop}(A /\ B) -> (B /\ A); intros; Refine H; diff --git a/lego/lego.el b/lego/lego.el index 24e1a63e..26b869cb 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -277,20 +277,9 @@ Given is the first SPAN which needs to be undone." ;; Commands specific to lego ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun lego-intros () - "intros." - (interactive) - (insert "intros ")) - -(defun lego-Intros () - "insert Intros." - (interactive) - (insert "Intros ")) - -(defun lego-Refine () - "Insert Refine." - (interactive) - (insert "Refine ")) +(proof-defshortcut lego-Intros "Intros " ?I) +(proof-defshortcut lego-intros "intros " ?i) +(proof-defshortcut lego-Refine "Refine " ?r) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Lego Indentation ;; @@ -397,10 +386,6 @@ Checks the width in the `proof-goals-buffer'" (proof-config-done) - (define-key (current-local-map) [(control c) ?i] 'lego-intros) - (define-key (current-local-map) [(control c) ?I] 'lego-Intros) - (define-key (current-local-map) [(control c) ?r] 'lego-Refine) - ;; outline (make-local-variable 'outline-regexp) diff --git a/plastic/plastic.el b/plastic/plastic.el index 4d15bf05..6ffcd217 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -297,20 +297,13 @@ Given is the first SPAN which needs to be undone." ;; Commands specific to plastic ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun plastic-intros () - "intros." - (interactive) - (insert (concat plastic-lit-string " intros "))) +(proof-defshortcut plastic-Intros + (concat plastic-lit-string " Intros ") ?I) +(proof-defshortcut plastic-intros + (concat plastic-lit-string " intros ") ?i) +(proof-defshortcut plastic-Refine + (concat plastic-lit-string " Refine ") ?i) -(defun plastic-Intros () - "List proof state." - (interactive) - (insert (concat plastic-lit-string " Intros "))) - -(defun plastic-Refine () - "List proof state." - (interactive) - (insert (concat plastic-lit-string " Refine "))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Plastic Indentation ;; @@ -436,20 +429,20 @@ Given is the first SPAN which needs to be undone." (proof-config-done) - (define-key (current-local-map) [(control c) ?i] 'plastic-intros) - (define-key (current-local-map) [(control c) ?I] 'plastic-Intros) - (define-key (current-local-map) [(control c) ?r] 'plastic-Refine) - ;; pcc macros etc - (define-key (current-local-map) [(control c) ?s] 'plastic-small-bar) - (define-key (current-local-map) [(control c) ?l] 'plastic-large-bar) - (define-key (current-local-map) [(control c) ?a] 'plastic-all-ctxt) + ;; da: I've changed this to use the new proof assitant specific keymap. + ;; (You can put these define keys at top level now) + (define-key proof-assistant-keymap ?s 'plastic-small-bar) + (define-key proof-assistant-keymap ?l 'plastic-large-bar) + (define-key proof-assistant-keymap ?a 'plastic-all-ctxt) ;; pcc over-ride the try-cmd fn (define-key (current-local-map) [(control c) (control t)] 'plastic-try-cmd) (define-key (current-local-map) [(control c) (control v)] 'plastic-minibuf) + + ;; FIXME da: these should probably be on the specific keymap too? (define-key (current-local-map) [(control c) (control o)] 'plastic-synchro) (define-key (current-local-map) [(control c) (control s)] 'plastic-show-shell) |