diff options
| -rw-r--r-- | CHANGES | 19 | ||||
| -rw-r--r-- | coq/coq-abbrev.el | 16 | ||||
| -rw-r--r-- | coq/coq.el | 27 |
3 files changed, 46 insertions, 16 deletions
@@ -21,14 +21,20 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. ** Coq changes +*** Multiple file handling for Coq Feature. + + No more experimental. Set coq-load-path to the list of directories + for libraries (you can attach it to the file using menu "coq prog + args"). + *** Support proof-tree visualization *** Indentation improvements using SMIE Still experimental. -** Limitations: +**** Limitations: -**** hard-wired precedence between bullets: - < + < * +***** hard-wired precedence between bullets: - < + < * example: Proof. - split. @@ -40,10 +46,9 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. - auto. Qed. -**** Always use "Proof." when proving an "Instance". - (wrong indentation and slow downs otherwise) - As a general rule, try to always introduce a proof with "Proof." - (or "Next Obligation"). +***** Always use "Proof." when proving an "Instance". (wrong + indentation and slow downs otherwise) As a general rule, try to + always introduce a proof with "Proof." (or "Next Obligation"). *** Minor parsing fixes @@ -51,6 +56,8 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. *** New commands for Print/Check/Show with Printing All flag +*** "Insert Requires" now uses completion based on coq-load-path + ** HOL Light [WORK IN PROGRESS] *** Basic support now works, see hol-light directory [WORK IN PROGRESS] diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index c279e91b..bc194d74 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -20,7 +20,7 @@ (defconst coq-tactics-menu (append '("Tactics (menu)" - ["Intros (smart)" coq-insert-intros t]) + ["Intros (smart)" coq-insert-intros :help "Insert \"intros h1 .. hn.\" where hi are the default names given by Coq."]) (coq-build-menu-from-db (append coq-tactics-db coq-solve-tactics-db)))) (defconst coq-tactics-abbrev-table @@ -80,6 +80,10 @@ (defpgdefault menu-entries `( ["Toggle 3 windows mode" proof-three-window-toggle t] + ["Toggle tooltips" proof-output-tooltips-toggle + :style toggle + :selected proof-output-tooltips + :help "Toggles tooltips (popup when hovering commands).\nSet `proof-output-tooltips' to nil to disable it by default."] "" ["Print..." coq-Print t] ["Check..." coq-Check t] @@ -118,16 +122,16 @@ ) "" ("INSERT" + ["Intros (smart)" coq-insert-intros :help "Insert \"intros h1 .. hn.\" where hi are the default names given by Coq."] "" ["tactic (interactive)" coq-insert-tactic t] - ,coq-tactics-menu ["tactical (interactive)" coq-insert-tactical t] - ,coq-tacticals-menu - "" ["command (interactive)" coq-insert-command t] - ,coq-commands-menu - "" ["term (interactive)" coq-insert-term t] + "" + ,coq-tactics-menu + ,coq-tacticals-menu + ,coq-commands-menu ,coq-terms-menu "" ["Module/Section (smart)" coq-insert-section-or-module t] @@ -2145,6 +2145,24 @@ mouse activation." '(("" 1) (":" 2) ("<:" 3)) "Enumerates the different kinds of type information for modules.") +(defun coq-postfix-.v-p (s) + (string-match-p "\\.v\\'" s)) + +(defun coq-directories-files (l) + (let* ((file-list-list (mapcar 'directory-files l)) + (file-list (apply 'append file-list-list)) + (filtered-list (remove-if-not 'coq-postfix-.v-p file-list))) + filtered-list)) + +(defun coq-remove-dot-v-extension (s) + (substring s 0 -2)) + +;; TODO cleanup composed elements of coq-load-path (-R option) +(defun coq-build-accessible-modules-list () + (let* ((pth (or coq-load-path '("."))) + (file-list (coq-directories-files pth))) + (mapcar 'coq-remove-dot-v-extension file-list))) + (defun coq-insert-section-or-module () "Insert a module or a section after asking right questions." (interactive) @@ -2178,10 +2196,11 @@ mouse activation." (completing-read "Command (TAB to see list, default Require Export) : " reqkinds-kinds-table nil nil nil nil "Require Export"))) - (setq s (read-string "Name (empty to stop) : ")) - (while (not (string-equal s "")) - (insert (format "%s %s.\n" reqkind s)) - (setq s (read-string "Name (empty to stop) : "))))) + (loop do + (setq s (completing-read "Name (empty to stop) : " + (coq-build-accessible-modules-list))) + (unless (zerop (length s)) (insert (format "%s %s.\n" reqkind s))) + while (not (string-equal s ""))))) (defun coq-end-Section () "Ends a Coq section." |