diff options
| -rw-r--r-- | coq/coq-abbrev.el | 48 | ||||
| -rw-r--r-- | coq/coq.el | 20 |
2 files changed, 33 insertions, 35 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index ba1c2f3d..8c034438 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -7,7 +7,7 @@ (require 'proof) (require 'coq-syntax) -(defun holes-show-doc () +(defun holes-show-doc () (interactive) (describe-variable 'holes-doc)) @@ -16,50 +16,50 @@ (describe-variable 'coq-local-vars-doc)) -(defconst coq-tactics-menu - (append '("INSERT TACTICS" +(defconst coq-tactics-menu + (append '("INSERT TACTICS" ["Intros (smart)" coq-insert-intros t]) (coq-build-menu-from-db (append coq-tactics-db coq-solve-tactics-db)))) -(defconst coq-tactics-abbrev-table +(defconst coq-tactics-abbrev-table (coq-build-abbrev-table-from-db (append coq-tactics-db coq-solve-tactics-db))) -(defconst coq-tacticals-menu +(defconst coq-tacticals-menu (append '("INSERT TACTICALS") (coq-build-menu-from-db coq-tacticals-db))) -(defconst coq-tacticals-abbrev-table +(defconst coq-tacticals-abbrev-table (coq-build-abbrev-table-from-db coq-tacticals-db)) -(defconst coq-commands-menu - (append '("INSERT COMMAND" +(defconst coq-commands-menu + (append '("INSERT COMMAND" ["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 +(defconst coq-commands-abbrev-table (coq-build-abbrev-table-from-db coq-commands-db)) -(defconst coq-terms-menu - (append '("INSERT TERM" +(defconst coq-terms-menu + (append '("INSERT TERM" ["Match (smart)" coq-insert-match t]) (coq-build-menu-from-db coq-terms-db))) -(defconst coq-terms-abbrev-table +(defconst coq-terms-abbrev-table (coq-build-abbrev-table-from-db coq-terms-db)) ;;; The abbrev table built from keywords tables ;#s and @{..} are replaced by holes by holes-abbrev-complete -(defun coq-install-abbrevs () +(defun coq-install-abbrevs () "install default abbrev table for coq if no other already is." (if (and (boundp 'coq-mode-abbrev-table) - (not (equal coq-mode-abbrev-table (make-abbrev-table)))) - (message "Coq abbrevs already exists, default not loaded") + (not (equal coq-mode-abbrev-table (make-abbrev-table)))) + (message "Coq abbrevs already exists, default not loaded") (define-abbrev-table 'coq-mode-abbrev-table - (append coq-tactics-abbrev-table coq-tacticals-abbrev-table - coq-commands-abbrev-table coq-terms-abbrev-table)) + (append coq-tactics-abbrev-table coq-tacticals-abbrev-table + coq-commands-abbrev-table coq-terms-abbrev-table)) ;; if we use default coq abbrev, never ask to save it (setq save-abbrevs nil) (message "Coq default abbrevs loaded") @@ -71,13 +71,13 @@ ;; The coq menu mainly built from tables -(defpgdefault menu-entries +(defpgdefault menu-entries `( ["Print..." coq-Print t] ["Check..." coq-Check t] ["About..." coq-About t] ["insert command (interactive)" coq-insert-command t] - ,coq-commands-menu + ,coq-commands-menu ["insert term (interactive)" coq-insert-term t] ,coq-terms-menu ["insert tactic (interactive)" coq-insert-tactic t] @@ -114,12 +114,12 @@ ["Print Scope/Visibility..." coq-PrintScope t] ) - ("Holes" + ("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 + ;; 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)" @@ -140,7 +140,7 @@ ["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 + ["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 @@ -150,7 +150,7 @@ ["help on setting persistently" coq-local-vars-list-show-doc t] )) -;; da: Moved this from the main menu to the Help submenu. +;; da: Moved this from the main menu to the Help submenu. ;; It also appears under Holes, anyway. (defpgdefault help-menu-entries '(["Tell me about holes?" holes-show-doc t] @@ -23,6 +23,10 @@ (require 'coq-local-vars) (require 'coq-syntax) ; determines coq version, sets coq-prog-name +;; ----- coq specific menu is defined in coq-abbrev.el +(require 'coq-abbrev) + + ;; ----- coq-shell configuration options @@ -89,7 +93,6 @@ To disable coqc being called (and use only make), set this to nil." ;; pc: 8.0 backward compliance: (if coq-version-is-V8-0 (setq proof-shell-unicode nil)) - (defcustom coq-prog-env nil "*List of environment settings d to pass to Coq process. On Windows you might need something like: @@ -216,14 +219,14 @@ On Windows you might need something like: (define-derived-mode coq-response-mode proof-response-mode "CoqResp" nil (coq-response-config))) - + (eval-and-compile - (define-derived-mode coq-mode proof-mode - "coq" - "Major mode for Coq scripts. + (define-derived-mode coq-mode proof-mode "coq" + "Major mode for Coq scripts. \\{coq-mode-map}" - (coq-mode-config))) + (coq-mode-config))) + (eval-and-compile (define-derived-mode coq-goals-mode proof-goals-mode @@ -642,7 +645,6 @@ happen since one of them is necessarily set to t in coq-syntax.el." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (defconst notation-print-kinds-table '(("Print Scope(s)" 0) ("Print Visibility" 1)) "Enumerates the different kinds of notation information one can ask to coq.") @@ -1243,7 +1245,6 @@ mouse activation." (while (re-search-forward "\(\w+[^\w]\)" nil t) (replace-match "\372\200\373\\1\374" nil t))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Context-senstive in-span menu additions @@ -1271,9 +1272,6 @@ mouse activation." ; Some smart insertion function ;;;;;;;;;;;;;;;;;;;;;; -;; ----- coq specific menu is defined in coq-abbrev.el -(require 'coq-abbrev) - (defconst module-kinds-table '(("Section" 0) ("Module" 1) ("Module Type" 2) ("Declare Module" 3)) "Enumerates the different kinds of modules.") |