diff options
| -rw-r--r-- | coq/coq-abbrev.el | 165 | ||||
| -rw-r--r-- | coq/coq.el | 2 | ||||
| -rw-r--r-- | generic/proof-syntax.el | 34 | ||||
| -rw-r--r-- | lib/holes.el | 2 |
4 files changed, 107 insertions, 96 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 0ab6bf71..7a24bf6c 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -17,7 +17,7 @@ (defconst coq-tactics-menu - (append '("INSERT TACTICS" + (append '("Tactics (menu)" ["Intros (smart)" coq-insert-intros t]) (coq-build-menu-from-db (append coq-tactics-db coq-solve-tactics-db)))) @@ -25,23 +25,24 @@ (coq-build-abbrev-table-from-db (append coq-tactics-db coq-solve-tactics-db))) (defconst coq-tacticals-menu - (append '("INSERT TACTICALS") + (append '("Tacticals (menu)") (coq-build-menu-from-db coq-tacticals-db))) (defconst coq-tacticals-abbrev-table (coq-build-abbrev-table-from-db coq-tacticals-db)) (defconst coq-commands-menu - (append '("INSERT COMMAND" - ["Module/Section (smart)" coq-insert-section-or-module t] - ["Require (smart)" coq-insert-requires t]) + (append '("Command (menu)" + ;["Module/Section (smart)" coq-insert-section-or-module t] + ;["Require (smart)" coq-insert-requires t] + ) (coq-build-menu-from-db coq-commands-db))) (defconst coq-commands-abbrev-table (coq-build-abbrev-table-from-db coq-commands-db)) (defconst coq-terms-menu - (append '("INSERT TERM" + (append '("Term (menu)" ["Match (smart)" coq-insert-match t]) (coq-build-menu-from-db coq-terms-db))) @@ -73,83 +74,95 @@ ;; The coq menu mainly built from tables (defpgdefault menu-entries - `( + `( + ["Toggle 3 windows mode" proof-three-window-toggle t] + "" + ["Print..." coq-Print t] + ["Check..." coq-Check t] + ["About..." coq-About t] + ("OTHER QUERIES" + ["Print Hint" coq-PrintHint t] + ["Show ith goal..." coq-Show t] + ["Show Tree" coq-show-tree t] + ["Show Proof" coq-show-proof t] + ["Show Conjectures" coq-show-conjectures t];; maybe not so useful with editing in PG? + "" ["Print..." coq-Print t] ["Check..." coq-Check t] ["About..." coq-About t] - ["insert command (interactive)" coq-insert-command t] - ,coq-commands-menu - ["insert term (interactive)" coq-insert-term t] - ,coq-terms-menu - ["insert tactic (interactive)" coq-insert-tactic t] + ["Search..." coq-SearchConstant t] + ["SearchRewrite..." coq-SearchRewrite t] + ["SearchAbout..." coq-SearchAbout t] + ["SearchPattern..." coq-SearchIsos t] + ["Locate constant..." coq-LocateConstant t] + ["Locate Library..." coq-LocateLibrary t] + ["Pwd" coq-Pwd t] + ["Inspect..." coq-Inspect t] + ["Print Section..." coq-PrintSection t] + "" + ["Locate notation..." coq-LocateNotation t] + ["Print Implicit..." coq-Print t] + ["Print Scope/Visibility..." coq-PrintScope t] + ) + "" + ("INSERT" + "" + ["tactic (interactive)" coq-insert-tactic t] ,coq-tactics-menu - ["insert tactical (interactive)" coq-insert-tactical t] + ["tactical (interactive)" coq-insert-tactical t] ,coq-tacticals-menu - - ;; da: I added Show sub menu, not sure if it's helpful, but why not. - ;; FIXME: submenus should be split off here. Also, these commands - ;; should only be available when a proof is open. - ;; pc: I added things in the show menu and called it QUERIES - ("OTHER QUERIES" - ["Print Hint" coq-PrintHint t] - ["Show ith goal..." coq-Show t] - ["Show Tree" coq-show-tree t] - ["Show Proof" coq-show-proof t] - ["Show Conjectures" coq-show-conjectures t];; maybe not so useful with editing in PG? - "" - ["Print..." coq-Print t] - ["Check..." coq-Check t] - ["About..." coq-About t] - ["Search..." coq-SearchConstant t] - ["SearchRewrite..." coq-SearchRewrite t] - ["SearchAbout..." coq-SearchAbout t] - ["SearchPattern..." coq-SearchIsos t] - ["Locate constant..." coq-LocateConstant t] - ["Locate Library..." coq-LocateLibrary t] - ["Pwd" coq-Pwd t] - ["Inspect..." coq-Inspect t] - ["Print Section..." coq-PrintSection t] - "" - ["Locate notation..." coq-LocateNotation t] - ["Print Implicit..." coq-Print t] - ["Print Scope/Visibility..." coq-PrintScope t] - ) - - ("Holes" - ;; da: I tidied this menu a bit. I personally think this "trick" - ;; of inserting strings to add documentation looks like a real - ;; mess in menus ... I've removed it for the three below since - ;; the docs below appear in popup in messages anyway. - ;; - ;; "Make a hole active click on it" - ;; "Disable a hole click on it (button 2)" - ;; "Destroy a hole click on it (button 3)" - ["Make hole at point" holes-set-make-active-hole t] - ["Make selection a hole" holes-set-make-active-hole t] - ["Replace active hole by selection" holes-replace-update-active-hole t] - ["Jump to active hole" holes-set-point-next-hole-destroy t] - ["Forget all holes in buffer" holes-clear-all-buffer-holes t] - ["Tell me about holes?" holes-show-doc t] - ;; look a bit better at the bottom - "Make hole with mouse: C-M-select" - "Replace hole with mouse: C-M-Shift select";; da: does this one work?? - ) - - ;; da: I also added abbrev submenu. Surprising Emacs doesn't have one? - ("Abbrevs" - ["Expand at point" expand-abbrev t] - ["Unexpand last" unexpand-abbrev t] - ["List abbrevs" list-abbrevs t] - ["Edit abbrevs" edit-abbrevs t];; da: is it OK to add edit? - ["Abbrev mode" abbrev-mode - :style toggle - :selected (and (boundp 'abbrev-mode) abbrev-mode)]) - ;; With all these submenus you have to wonder if these things belong - ;; on the main menu. Are they the most often used? - ["Compile" coq-Compile t] + "" + ["command (interactive)" coq-insert-command t] + ,coq-commands-menu + "" + ["term (interactive)" coq-insert-term t] + ,coq-terms-menu + "" + ["Module/Section (smart)" coq-insert-section-or-module t] + ["Require (smart)" coq-insert-requires t]) + ;; da: I added Show sub menu, not sure if it's helpful, but why not. + ;; FIXME: submenus should be split off here. Also, these commands + ;; should only be available when a proof is open. + ;; pc: I added things in the show menu and called it QUERIES + + "" + ("HOLES" + ;; da: I tidied this menu a bit. I personally think this "trick" + ;; of inserting strings to add documentation looks like a real + ;; mess in menus ... I've removed it for the three below since + ;; the docs below appear in popup in messages anyway. + ;; + ;; "Make a hole active click on it" + ;; "Disable a hole click on it (button 2)" + ;; "Destroy a hole click on it (button 3)" + ["Make hole at point" holes-set-make-active-hole t] + ["Make selection a hole" holes-set-make-active-hole t] + ["Replace active hole by selection" holes-replace-update-active-hole t] + ["Jump to active hole" holes-set-point-next-hole-destroy t] + ["Forget all holes in buffer" holes-clear-all-buffer-holes t] + ["Tell me about holes?" holes-show-doc t] + ;; look a bit better at the bottom + "Make hole with mouse: C-M-select" + "Replace hole with mouse: C-M-Shift select";; da: does this one work?? + ) + + ;; da: I also added abbrev submenu. Surprising Emacs doesn't have one? + ("ABBREVS" + ["Expand at point" expand-abbrev t] + ["Unexpand last" unexpand-abbrev t] + ["List abbrevs" list-abbrevs t] + ["Edit abbrevs" edit-abbrevs t];; da: is it OK to add edit? + ["Abbrev mode" abbrev-mode + :style toggle + :selected (and (boundp 'abbrev-mode) abbrev-mode)]) + ;; With all these submenus you have to wonder if these things belong + ;; on the main menu. Are they the most often used? + "" + ("COQ PROG (ARGS)" ["Set coq prog *persistently*" coq-ask-insert-coq-prog-name t] ["help on setting persistently" coq-local-vars-list-show-doc t] - )) + ["Compile" coq-Compile t]) + )) ;; da: Moved this from the main menu to the Help submenu. ;; It also appears under Holes, anyway. @@ -1456,8 +1456,6 @@ be asked to the user." (define-key coq-keymap [(control ?h)] 'coq-PrintHint) (define-key coq-keymap [(control ?l)] 'coq-LocateConstant) (define-key coq-keymap [(control ?n)] 'coq-LocateNotation) -;(define-key coq-keymap [?'] 'coq-highlight-error) - ;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index 87831f50..b31c040b 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -27,7 +27,7 @@ (defconst proof-no-regexp "\\'\\`" "A regular expression that never matches anything") - + (defun proof-regexp-alt (&rest args) "Return the regexp which matches any of the regexps ARGS." @@ -155,9 +155,9 @@ Default is comma separated, or SEPREGEXP if set." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;; A function to unfontify commas in declarations and definitions. -;; Useful for provers which have declarations of the form x,y,z:Ty -;; All that can be said for it is that the previous ways of doing +;; A function to unfontify commas in declarations and definitions. +;; Useful for provers which have declarations of the form x,y,z:Ty +;; All that can be said for it is that the previous ways of doing ;; this were even more bogus.... (defun proof-zap-commas (limit) @@ -222,18 +222,18 @@ return the resulting (string) value." ((functionp string) (funcall string filename)) (t - (proof-format - (list (cons "%s" (proof-format proof-shell-filename-escapes + (proof-format + (list (cons "%s" (proof-format proof-shell-filename-escapes (expand-file-name filename))) - (cons "%e" (proof-format proof-shell-filename-escapes + (cons "%e" (proof-format proof-shell-filename-escapes (expand-file-name filename))) - (cons "%r" (proof-format proof-shell-filename-escapes + (cons "%r" (proof-format proof-shell-filename-escapes filename)) - (cons "%m" (proof-format proof-shell-filename-escapes - (file-name-nondirectory + (cons "%m" (proof-format proof-shell-filename-escapes + (file-name-nondirectory (file-name-sans-extension filename))))) string)))) - + ;; ;; Functions for inserting text into buffer. @@ -260,11 +260,11 @@ Any other %-prefixed character inserts itself." (setq acc (concat acc (char-to-string ch))) (setq i (1+ i)) (setq ch (elt text i)) - (cond ;((eq ch ?l) + (cond ;((eq ch ?l) ; (setq acc (concat acc isa-logic-name))) - ;((eq ch ?s) - ; (setq acc - ; (concat acc + ;((eq ch ?s) + ; (setq acc + ; (concat acc ; (int-to-string ; (if (boundp 'isa-denoted-subgoal) ; isa-denoted-subgoal @@ -273,7 +273,7 @@ Any other %-prefixed character inserts itself." ; (if acc (insert acc)) ; (setq acc nil) ; (comint-send-input)) - ((eq ch ?p) + ((eq ch ?p) (if acc (insert acc)) (setq acc nil) (setq pos (point))) @@ -289,7 +289,7 @@ Any other %-prefixed character inserts itself." (while strings (setq stringsep (concat stringsep (car strings))) (setq strings (cdr strings)) - (if strings (setq stringsep + (if strings (setq stringsep (concat stringsep sep)))) stringsep)) diff --git a/lib/holes.el b/lib/holes.el index 87ef86dc..8fe9139f 100644 --- a/lib/holes.el +++ b/lib/holes.el @@ -760,7 +760,7 @@ This keymap is used only when (define-key map [(control c) (control y)] 'holes-replace-update-active-hole) (define-key map [(control meta down-mouse-1)] 'holes-mouse-set-make-active-hole) (define-key map [(control meta shift down-mouse-1)] 'holes-mouse-replace-active-hole) - (define-key map [(meta return)] 'holes-set-point-next-hole-destroy) + (define-key map [(control c) (control j)] 'holes-set-point-next-hole-destroy) map) "Keymap of `holes-mode'. This is not the keymap used on holes's overlay |