diff options
Diffstat (limited to 'generic')
| -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 |
4 files changed, 79 insertions, 7 deletions
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." |