diff options
| -rw-r--r-- | coq/coq-abbrev.el | 1 | ||||
| -rw-r--r-- | coq/coq-db.el | 6 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 19 | ||||
| -rw-r--r-- | coq/coq.el | 5 |
4 files changed, 18 insertions, 13 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 6f156a8c..ba1c2f3d 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -31,7 +31,6 @@ (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] diff --git a/coq/coq-db.el b/coq/coq-db.el index d575ad09..627ec241 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -138,7 +138,7 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See (spaces (make-string entry-with ? )) ;;(restofmenu (coq-build-menu-from-db-internal tl (- size 1) menuwidth)) ) - (when (not e7) ; if not hidden + (when (not e7) ;; if not hidden (let ((menu-entry (vector ;; menu entry label @@ -171,8 +171,8 @@ for DB structure." "Take a keyword database DB and return a list of insertion menus for them. Submenus contain SIZE entries (default 30). See `coq-syntax-db' for DB structure." - (let* ((l (coq-sort-menu-entries db)) (res - ()) + ;; sort is destructive for the list, so copy list before sorting + (let* ((l (coq-sort-menu-entries (copy-list db))) (res ()) (wdth (+ 2 (max-length-db db))) (sz (or size 30)) (lgth (length l))) (while l diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 72190872..ec17d506 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -463,7 +463,7 @@ ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary") ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t) ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t) - ("Definition" "def" "Definition #:# := #." t "Definition");; careful + ("Definition goal" "defg" "Definition #:#.\n#\nSave." t);; careful ("Fact" "fct" "Fact # : #." t "Fact") ("Goal" nil "Goal #." t "Goal") ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma") @@ -482,9 +482,8 @@ "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. " ) -(defvar coq-commands-db - (append - coq-user-commands-db +;; command that are not declarations, definition or goal starters +(defvar coq-other-commands-db '( ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu ("About" nil "About #." nil "About") @@ -602,12 +601,18 @@ ("Unset Printing Coercions" nil "Unset Printing Coercions." nil "Unset\\s-+Printing\\s-+Coercions") ("Unset Printing Notations" "unsprn" "Unset Printing Notations" nil "Unset\\s-+Printing\\s-+Notations") ("Unset Undo" nil "Unset Undo." nil "Unset\\s-+Undo") - ; ("print" "pr" "print #" "print") - ) - coq-decl-db coq-defn-db coq-goal-starters-db) + ; ("print" "pr" "print #" "print") + ) + "Command that are not declarations, definition or goal starters." + ) + +(defvar coq-commands-db + (append coq-decl-db coq-defn-db coq-goal-starters-db + coq-other-commands-db coq-user-commands-db) "Coq all commands keywords information list. See `coq-syntax-db' for syntax. " ) + (defvar coq-terms-db '( ("fun (1 args)" "f" "fun #:# => #" nil "fun") @@ -86,6 +86,9 @@ To disable coqc being called (and use only make), set this to nil." ;; library `un-define' to work on xemacs." ;; (or (boundp 'proof-shell-unicode) (setq proof-shell-unicode nil)) ;; da: I think the default t setting now works fine, at least for me. +;; 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. @@ -940,8 +943,6 @@ To be used in `proof-shell-process-output-system-specific'." ))) - - (defun coq-shell-mode-config () (setq proof-shell-prompt-pattern coq-shell-prompt-pattern |