diff options
| -rw-r--r-- | CHANGES | 18 | ||||
| -rw-r--r-- | coq/coq-abbrev.el | 1 | ||||
| -rw-r--r-- | coq/coq-db.el | 45 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 54 | ||||
| -rw-r--r-- | coq/coq.el | 14 |
5 files changed, 103 insertions, 29 deletions
@@ -116,7 +116,20 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. Experimental: colorize hypothesis names and some parts of error and warning messages. For readability. -*** mouse Queries +*** Coq Querying facilities + +**** Minibuffer interactive queries + + Menu Coq/Other Queries (C-c C-a C-q) allows to send queries (like + Print, Locate...) (à la auctex) without inserting them in the + buffer. Queries are TAB completed and the usual history mechanism + applies. Completion allows only a set of state preserving + commands. The list is not exhaustive yet. + + This should replace the C-c C-v usual command mechanism (which has + no completion). + +**** Mouse Queries This remaps standard emacs key bindings (faces and buffers menus popup), so this is not enabled by default, use (setq @@ -128,7 +141,8 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. that id. As most of the bindings, they are active in the three buffer - (script, goals, response). + (script, goals, response). Obeys C-u prefix for "Printing all" + flag. *** bug fixes - Annoying cursor jump when hitting ".". diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 2ccf5cab..431f463f 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -132,6 +132,7 @@ ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"] ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"] ["About..." coq-About :help "With prefix arg (C-u): Set Printing All first"] + ["Other..." coq-query] [ "Store Response" proof-store-response-win :help "Stores the content of response buffer in a dedicated buffer"] [ "Store Goal" proof-store-goals-win :help "Stores the content of goals buffer in a dedicated buffer"] ("OTHER QUERIES" diff --git a/coq/coq-db.el b/coq/coq-db.el index 3985a588..d90d3b58 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -67,11 +67,12 @@ Explanation of the first line: the tactic menu entry mytac, abbreviated by mt, will insert \"mytac # #\" where #s are holes to fill, and \"mytac\" becomes a new keyword to colorize.") -(defun coq-insert-from-db (db prompt) +(defun coq-insert-from-db (db prompt &optional alwaysjump) "Ask for a keyword, with completion on keyword database DB and insert. -Insert corresponding string with holes at point. If an insertion function is -present for the keyword, call it instead. see `coq-syntax-db' for DB -structure." +Insert corresponding string with holes at point. If an insertion +function is present for the keyword, call it instead. see +`coq-syntax-db' for DB structure. If ALWAYSJUMP is non nil, jump +to the first hole even if more than one." (let* ((tac (completing-read (concat prompt " (TAB for completion): ") db nil nil)) (infos (cddr (assoc tac db))) @@ -80,11 +81,45 @@ structure." (pt (point))) (if f (funcall f) ; call f if present (insert (or s tac)) ; insert completion and indent otherwise - (holes-replace-string-by-holes-backward-jump pt) + (holes-replace-string-by-holes-backward-jump pt nil alwaysjump) (indent-according-to-mode)))) +(defun coq-build-command-from-db (db prompt &optional preformatquery) + "Ask for a keyword, with completion on keyword database DB and send to coq. +See `coq-syntax-db' for DB structure." + ;; Next invocation of minibuffer (read-string below) will first recursively + ;; ask for a command in db and expand it with holes. This way the cursor will + ;; be at the right place. + (minibuffer-with-setup-hook + (lambda () (coq-insert-from-db db prompt t)) + ;; I use recursive edition on the minibuffer here, because I want the cursor + ;; to be moved inside the initial content + (let ((enable-recursive-minibuffers t)) ; invo + (read-string (concat prompt " : ")) +; (read-from-minibuffer (concat prompt " : ")) + ))) +; +;(defun coq-build-command-from-db (db prompt &optional preformatquery) +; "Ask for a keyword, with completion on keyword database DB and send to coq. +;See `coq-syntax-db' for DB structure." +; (let* ((query (completing-read (concat prompt " (TAB for completion): ") +; db nil nil)) +; (infos (cddr (assoc query db))) +; (s (car infos)) +; ; default format is add a space at the end of query, for arguments. +; (preformat (or preformatquery '(lambda (s) (concat s " ")))) +; (initialvalue (funcall preformat query)) +; (whole-query +; (minibuffer-with-setup-hook +; 'coq-move-cursor-at-sharp +; (read-string (concat prompt " : ") initialvalue t nil)))) +; whole-query)) +; + + + (defun coq-build-regexp-list-from-db (db &optional filter) "Take a keyword database DB and return the list of regexps for font-lock. If non-nil Optional argument FILTER is a function applying to each line of DB. diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 9075c1e1..c845574c 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -502,6 +502,37 @@ so for the following reasons: "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. " ) +;; TODO: dig other queries from the refman. +(defvar coq-queries-commands-db + '( + ("About" nil "About #." nil "About") + ("Check" nil "Check" nil "Check") + ("Inspect" nil "Inspect #." nil "Inspect") + ("Locate File" nil "Locate File \"#\"." nil "Locate\\s-+File") + ("Locate Library" nil "Locate Library #." nil "Locate\\s-+Library") + ("Locate Notation" nil "Locate Notation (#) #" nil "Locate\\s-+Notation") + ("Locate" nil "Locate" nil "Locate") + ("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions") + ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint) + ("Print" "p" "Print #." nil "Print") + ("Pwd" nil "Pwd." nil "Pwd") + ("Search" nil "Search #" nil "Search") + ("SearchAbout" nil "SearchAbout #" nil "SearchAbout") + ("SearchPattern" nil "SearchPattern (#)" nil "SearchPattern") + ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite") + ("Show" nil "Show #." nil "Show") + ("Test" nil "Test" nil "Test" nil t) + ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth") + ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If") + ("Test Printing Let" nil "Test Printing Let #." nil "Test\\s-+Printing\\s-+Let") + ("Test Printing Synth" nil "Test Printing Synth." nil "Test\\s-+Printing\\s-+Synth") + ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width") + ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard") + ) + "Coq queries command, that deserve a separate menu for sending them to coq without insertion. " + ) + + ;; command that are not declarations, definition or goal starters (defvar coq-other-commands-db '( @@ -509,7 +540,6 @@ so for the following reasons: ("BeginSubproof" "bs" "BeginSubproof.\n#\nEndSubproof." t "BeginSubproof") ("EndSubproof" "es" "EndSubproof.#" t "EndSubproof") ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu - ("About" nil "About #." nil "About") ; ("Add" nil "Add #." nil "Add" nil t) ("Add Abstract Ring" nil "Add Abstract Ring #." t "Add\\s-+Abstract\\s-+Ring") ("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t "Add\\s-+Abstract\\s-+Semi\\s-+Ring") @@ -529,7 +559,6 @@ so for the following reasons: ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") ("Cd" nil "Cd #." nil "Cd") - ("Check" nil "Check" nil "Check") ("Local Close Scope" "lclsc" "Local Close Scope #" t "Local\\s-+Close\\s-+Scope") ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope") ("Comments" nil "Comments #." nil "Comments") @@ -556,10 +585,6 @@ so for the following reasons: ("Implicit Types" nil "Implicit Types # : #." t "Implicit\\s-+Types") ("Import" nil "Import #." t "Import") ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") - ("Inspect" nil "Inspect #." nil "Inspect") - ("Locate File" nil "Locate File \"#\"." nil "Locate\\s-+File") - ("Locate Library" nil "Locate Library #." nil "Locate\\s-+Library") - ("Locate" nil "Locate" nil "Locate") ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t) ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t) ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t) @@ -575,11 +600,7 @@ so for the following reasons: ("Open Local Scope" nil "Open Local Scope #" t "Open\\s-+Local\\s-+Scope") ("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope") ("Preterm" nil "Preterm." nil "Preterm") - ("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions") - ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint) - ("Print" "p" "Print #." nil "Print") ("Qed" nil "Qed." nil "Qed") - ("Pwd" nil "Pwd." nil "Pwd") ("Recursive Extraction" "recextr" "Recursive Extraction @{id}." nil "Recursive\\s-+Extraction") ("Recursive Extraction Library" "recextrl" "Recursive Extraction Library @{id}." nil "Recursive\\s-+Extraction\\s-+Library") ("Recursive Extraction Module" "recextrm" "Recursive Extraction Module @{id}." nil "Recursive\\s-+Extraction\\s-+Module") @@ -593,10 +614,6 @@ so for the following reasons: ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation") ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline") ("Save" nil "Save." t "Save") - ("Search" nil "Search #" nil "Search") - ("SearchAbout" nil "SearchAbout #" nil "SearchAbout") - ("SearchPattern" nil "SearchPattern #" nil "SearchPattern") - ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite") ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Set\\s-+Extraction\\s-+AutoInline") ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Set\\s-+Extraction\\s-+Optimize") ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Set\\s-+Implicit\\s-+Arguments") @@ -608,16 +625,8 @@ so for the following reasons: ("Set Printing Coercions" nil "Set Printing Coercions." t "Set\\s-+Printing\\s-+Coercions") ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations") ("Set Undo" nil "Set Undo #." nil "Set\\s-+Undo") - ("Show" nil "Show #." nil "Show") ("Solve Obligations" "oblssolve" "Solve Obligations using #." t "Solve\\s-+Obligations") ("Tactic Notation" nil "Tactic Notation # := #." t "Tactic\\s-+Notation") - ("Test" nil "Test" nil "Test" nil t) - ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth") - ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If") - ("Test Printing Let" nil "Test Printing Let #." nil "Test\\s-+Printing\\s-+Let") - ("Test Printing Synth" nil "Test Printing Synth." nil "Test\\s-+Printing\\s-+Synth") - ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width") - ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard") ("Transparent" nil "Transparent #." nil "Transparent") ("Unfocus" nil "Unfocus." nil "Unfocus") @@ -645,6 +654,7 @@ so for the following reasons: (defvar coq-commands-db (append coq-decl-db coq-defn-db coq-goal-starters-db + coq-queries-commands-db coq-other-commands-db coq-ssreflect-commands-db coq-user-commands-db) "Coq all commands keywords information list. See `coq-syntax-db' for syntax. " ) @@ -2112,6 +2112,17 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (interactive) (coq-insert-from-db coq-terms-db "Kind of term")) + +(defun coq-query (showall) + "Ask for a query, with completion, and send to Coq." + (interactive "P") + (let ((q (coq-build-command-from-db coq-queries-commands-db "which Query?"))) + (if showall + (coq-command-with-set-unset + "Set Printing All" q "Unset Printing All" nil "Test Printing All") + (proof-shell-invisible-command q)))) + + ;; Insertion commands (define-key coq-keymap [(control ?i)] 'coq-insert-intros) (define-key coq-keymap [(control ?m)] 'coq-insert-match) @@ -2122,6 +2133,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-keymap [?!] 'coq-insert-solve-tactic) ; will work in tty (define-key coq-keymap [(control ?\s)] 'coq-insert-term) (define-key coq-keymap [(control return)] 'coq-insert-command) +(define-key coq-keymap [(control ?q)] 'coq-query) (define-key coq-keymap [(control ?r)] 'coq-insert-requires) ; Query commands @@ -2154,6 +2166,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-goals-mode-map [(control ?c)(control ?a)?r] 'proof-store-response-win) (define-key coq-goals-mode-map [(control ?c)(control ?a)?g] 'proof-store-goals-win) (define-key coq-goals-mode-map [(control ?c)(control ?a)?h] 'coq-PrintHint) +(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?q)] 'coq-query) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?c)] 'coq-Check) @@ -2165,6 +2178,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?r)] 'proof-store-response-win) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?g)] 'proof-store-goals-win) (define-key coq-response-mode-map [(control ?c)(control ?a)?h] 'coq-PrintHint) +(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?q)] 'coq-query) (when coq-remap-mouse-1 (define-key proof-mode-map [(control down-mouse-1)] 'coq-id-under-mouse-query) |