diff options
| -rw-r--r-- | CHANGES | 9 | ||||
| -rw-r--r-- | coq/coq-abbrev.el | 1 | ||||
| -rw-r--r-- | coq/coq.el | 77 |
3 files changed, 60 insertions, 27 deletions
@@ -142,6 +142,15 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac file contains "Require ... ssreflect" on the same line; otherwise PG inserts "intros ..." as before. +*** Customizing Search Blacklist (command created and menu entry moved) + To change the list of blacklisted string for Search commands + during development, use now + coq-change-search-blacklist-interactive. The menu for this has + moved, it is now in Coq/Other Queries/Search Blacklist. + + To change the default blacklist, set variable + coq-search-blacklist-string (unchanged). + *** bug fixes - avoid leaving partial files behind when compilation fails - 123: Parallel background compliation fails to execute some diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index edeb0616..4d0adedb 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -320,6 +320,7 @@ ["Search..." coq-Search t] ["SearchRewrite..." coq-SearchRewrite t] ["SearchPattern..." coq-SearchIsos t] + ["Search Blacklist..." coq-change-search-blacklist-interactive t] ["Locate constant..." coq-LocateConstant t] ["Locate Library..." coq-LocateLibrary t] ["Pwd" coq-Pwd t] @@ -91,28 +91,40 @@ These are appended at the end of `coq-shell-init-cmd'." ;; Default coq is only Private_ and _subproof (defcustom coq-search-blacklist-string ; add this? \"_ind\" \"_rect\" \"_rec\" "\"Private_\" \"_subproof\"" - "String for blacklisting strings from requests to Coq environment." + "Initial strings to blacklist in requests to Coq environment. +If you are setting this via emacs cutomization menus, you should +restart Coq to see the effect. To change blacklist during a coq +development, please use \\[coq-change-search-blacklist-interactive] +instead (or menu: Coq/Settings/Search Blacklist)." :type 'string :group 'coq) +;; Coq has no command to overwrite the current blacklist, only to add or remove +;; particular strings. To provide the overwrite feature to the user we thus need +;; to know the current value of blacklist to first remove everything, then add +;; the new values. +;;; TODO: retrieve the value from coq itself and remove this variable? +(defvar coq-search-blacklist-current-string coq-search-blacklist-string + "Current value of Coq Search Blacklist. +This may become desynchronized with Coq if you use the command +\"Add/Remove Search Blacklist\" in you script." ) + (defcustom coq-prefer-top-of-conclusion nil "Prefer start of the conclusion over its end when displaying large goals. Namely, goals that do not fit in the goals window." :type 'boolean :group 'coq) -;; this remembers the previous value of coq-search-blacklist-string, so that we -;; can cook a remove+add blacklist command each time the variable is changed. -;; initially we put it at current value of coq-search-blacklist-string. -(defvar coq-search-blacklist-string-prev coq-search-blacklist-string) -;TODO: remove Set Undo xx. It is obsolete since coq-8.5 at least. -;;`(,(format "Set Undo %s . " coq-default-undo-limit) "Set Printing Width 75.") (defconst coq-shell-init-cmd - (append `(,(format "Add Search Blacklist %s. " coq-search-blacklist-string)) - '("Set Suggest Proof Using. ") - coq-user-init-cmd) - "Command to initialize the Coq Proof Assistant.") + (append + `( + ;; Should this variable be buffer-local? No opinion on that but if yes we + ;; should re-intialize to coq-search-blacklist-string instead of + ;; keeping the current value (that may come from another file). + ,(format "Add Search Blacklist %s. " coq-search-blacklist-current-string)) + '("Set Suggest Proof Using. ") coq-user-init-cmd) + "Command to initialize the Coq Proof Assistant.") (require 'coq-syntax) @@ -2153,22 +2165,33 @@ Set Diffs setting if Coq is running and has a version >= 8.10." ;; :type 'integer ;; :setting "Set Undo %i . ") -(defun coq-set-search-blacklist (s) - (let ((res (format "Remove Search Blacklist %s. \nAdd Search Blacklist %s. " - coq-search-blacklist-string-prev s))) - (setq coq-search-blacklist-string-prev coq-search-blacklist-string) - res)) - - -(defun coq-get-search-blacklist (s) - coq-search-blacklist-string) - - -(defpacustom search-blacklist coq-search-blacklist-string - "Strings to blacklist in requests to Coq environment." - :type 'string - :get 'coq-get-search-blacklist - :setting coq-set-search-blacklist) +;; Problem if the Remove or Add fails we leave Coq's blacklist in a strange +;; state: unnoticed by the user, and desynched from +;; coq-search-blacklist-current-string. +;; TODO: have a way to detect error and re-set old value. +(defun coq-change-search-blacklist (s) + (let* ((cmd-clean (list (format "Remove Search Blacklist %s." + coq-search-blacklist-current-string))) + (item-clean `(nil ,cmd-clean proof-done-invisible 'invisible)) + (cmd-set (list (format "Add Search Blacklist %s." s))) + (item-set `(nil ,cmd-set proof-done-invisible 'invisible))) + (proof-add-to-queue `(,item-clean ,item-set) 'advancing))) + +(defun coq-change-search-blacklist-interactive () + (interactive) + (proof-shell-ready-prover) + (let* ((current-value coq-search-blacklist-current-string) + (s (read-string + "Set search blacklist to: " + current-value 'proof-minibuffer-history))) + (coq-change-search-blacklist s) + (setq coq-search-blacklist-current-string s))) + +;; (defpacustom search-blacklist coq-search-blacklist-string +;; "Strings to blacklist in requests to Coq environment." +;; :type 'string +;; :get 'coq-get-search-blacklist +;; :setting coq-set-search-blacklist) (defpacustom time-commands nil |