diff options
| -rw-r--r-- | coq/coq-system.el | 12 | ||||
| -rw-r--r-- | coq/coq.el | 112 | ||||
| -rw-r--r-- | generic/proof-tree.el | 13 |
3 files changed, 127 insertions, 10 deletions
diff --git a/coq/coq-system.el b/coq/coq-system.el index 88ce06be..0b9b6c58 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -170,6 +170,18 @@ Returns nil if the version can't be detected." (signal 'coq-unclassifiable-version coq-version-to-use)) (t (signal (car err) (cdr err)))))))) +(defun coq--post-v86 () + "Return t if the auto-detected version of Coq is >= 8.6. +Return nil if the version cannot be detected." + (let ((coq-version-to-use (or (coq-version t) "8.5"))) + (condition-case err + (not (coq--version< coq-version-to-use "8.6")) + (error + (cond + ((equal (substring (cadr err) 0 15) "Invalid version") + (signal 'coq-unclassifiable-version coq-version-to-use)) + (t (signal (car err) (cdr err)))))))) + (defcustom coq-use-makefile nil "Whether to look for a Makefile to attempt to guess the command line. Set to t if you want this feature, but note that it is deprecated." @@ -24,6 +24,8 @@ (defvar proof-info nil) ; dynamic scope in proof-tree-urgent-action (defvar action nil) ; dynamic scope in coq-insert-as stuff (defvar string nil) ; dynamic scope in coq-insert-as stuff + (defvar old-proof-marker nil) + ; dynamic scoq in coq-proof-tree-enable-evar-callback (defvar coq-auto-insert-as nil) ; defpacustom (defvar coq-time-commands nil) ; defpacustom (defvar coq-use-project-file t) ; defpacustom @@ -1851,14 +1853,19 @@ not finished, because Coq 8.5 lists open existential variables as (new) open subgoals. For this test we assume that `proof-marker' has not yet been moved. +The `proof-tree-urgent-action-hook' is also called for undo +commands. For those, nothing is done. + The not yet delayed output is in the region \[proof-shell-delayed-output-start, proof-shell-delayed-output-end]." ;; (message "CPTGNS start %s end %s" ;; proof-shell-delayed-output-start ;; proof-shell-delayed-output-end) - (with-current-buffer proof-shell-buffer - (let ((start proof-shell-delayed-output-start) - (end proof-shell-delayed-output-end)) + (let ((start proof-shell-delayed-output-start) + (end proof-shell-delayed-output-end) + (state (car proof-info))) + (when (> state proof-tree-last-state) + (with-current-buffer proof-shell-buffer ;; The message "All the remaining goals are on the shelf" is processed as ;; urgent message and is therefore before ;; proof-shell-delayed-output-start. We therefore need to go back to @@ -1879,7 +1886,7 @@ The not yet delayed output is in the region '(no-goals-display no-response-display proof-tree-show-subgoal)) - proof-action-list))))))))) + proof-action-list)))))))))) (add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-get-new-subgoals) @@ -1916,6 +1923,103 @@ This is the Coq incarnation of `proof-tree-find-undo-position'." (span-start span-res))) +;; In Coq 8.6 the evar line is disabled by default because on some proofs it +;; causes a severe performance hit. The disabled evar line causes prooftree to +;; crash with a parsing error. Proof General must therefore turn on the evar +;; output with the command "Set Printing Dependent Evars Line". Of course, +;; after the proof, the evar line must be set back to what it was before the +;; proof. I therefore look in the urgent action hook if proof display is +;; switched on or off. When switched on, I test the current evar printing +;; status with the undodumented command "Test Printing Dependent Evars Line" to +;; remember if I have to switch evar printing off eventually. + +(defvar coq--proof-tree-must-disable-evars nil + "Remember if evar printing must be disabled when leaving the current proof.") + +(defun coq-proof-tree-enable-evar-callback (span) + "Callback for the evar printing status test. +This is the callback for the command ``Test Printing Dependent +Evars Line''. It checks whether evar printing was off and +remembers that fact in `coq--proof-tree-must-disable-evars'." + (with-current-buffer proof-shell-buffer + (save-excursion + ;; When the callback runs, the next item is sent to Coq already and + ;; therefore proof-marker points to the end of the next command + ;; already. proof-shell-filter-manage-output sets old-proof-marker + ;; before calling proof-shell-exec-loop, this therefore points to the + ;; end of the command of this callback. + (goto-char old-proof-marker) + (when (re-search-forward "The Printing Dependent Evars Line mode is " + nil t) + (if (looking-at "off") + (progn + ;; (message "CPTEEC evar line mode was off") + (setq coq--proof-tree-must-disable-evars t)) + ;; (message "CPTEEC evar line mode was on") + (setq coq--proof-tree-must-disable-evars nil)))))) + +(defun coq-proof-tree-insert-evar-command (cmd &optional callback) + "Insert an evar printing command at the head of `proof-action-list'." + (push (proof-shell-action-list-item + (concat cmd " Printing Dependent Evars Line.") + (if callback callback 'proof-done-invisible) + (list 'invisible)) + proof-action-list)) + +(defun coq-proof-tree-enable-evars () + "Enable the evar status line for Coq >= 8.6. +Test the status of evar printing to be able to set it back +properly after the proof and enable the evar printing." + (when (coq--post-v86) + ;; We push to proof-action-list --- therefore we need to push in reverse + ;; order! + (coq-proof-tree-insert-evar-command "Set") + (coq-proof-tree-insert-evar-command + "Test" + 'coq-proof-tree-enable-evar-callback))) + +(defun coq-proof-tree-disable-evars () + "Disable evar printing if necessary. +This function switches off evar printing after the proof, if it +was off before the proof. For undo commands, we rely on the fact +that Coq itself undos the effect of the evar printing change that +we inserted after the goal statement. We also rely on the fact +that Proof General never backtracks into the middle of a +proof. (If this would happen, Coq would switch evar printing on +and the code here would not switch it off after the proof.) + +Being called from `proof-tree-urgent-action-hook', this function +can rely on `proof-info' being dynamically bound to the last +result of `coq-proof-tree-get-proof-info'." + (when coq--proof-tree-must-disable-evars + (when (> (car proof-info) proof-tree-last-state) + (coq-proof-tree-insert-evar-command "Unset")) + (setq coq--proof-tree-must-disable-evars nil))) + +(defun coq-proof-tree-evar-display-toggle () + "Urgent action hook function for changing the evar printing status in Coq. +This function is for `proof-tree-urgent-action-hook' (which is +called only if external proof disaply is switched on). It checks +whether a proof was started or stopped and inserts commands for +enableing and disabling the evar status line for Coq 8.6 or +later. Without the evar status line being enabled, prooftree +crashes. + +Must only be called via `proof-tree-urgent-action-hook' to ensure +that the dynamic variable `proof-info' is bound to the current +result of `coq-proof-tree-get-proof-info'." + (let ((current-proof-name (cadr proof-info))) + (cond + ((and (null proof-tree-current-proof) current-proof-name) + ;; started a new proof + (coq-proof-tree-enable-evars)) + ((and proof-tree-current-proof (null current-proof-name)) + ;; finished the current proof + (coq-proof-tree-disable-evars))))) + +(add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-evar-display-toggle) + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Pre-processing of input string diff --git a/generic/proof-tree.el b/generic/proof-tree.el index 77d3cc33..f0894656 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -842,13 +842,14 @@ The not yet delayed output is in the region (start proof-shell-delayed-output-start) (end proof-shell-delayed-output-end) inst-ex-vars) - (when (and (not (memq 'proof-tree-show-subgoal flags)) - (> state proof-tree-last-state)) - ;; Only deal with existentials if the proof assistant has them - ;; (i.e., proof-tree-existential-regexp is set) and if there are some - ;; goals with existentials. - (when (and proof-tree-existential-regexp + (unless (memq 'proof-tree-show-subgoal flags) + (when (and (> state proof-tree-last-state) + proof-tree-existential-regexp proof-tree-existentials-alist) + ;; Only deal with existentials if this is not and undo + ;; command, if the proof assistant actually has existentials + ;; (i.e., proof-tree-existential-regexp is set) and if there + ;; are some goals with existentials. (setq inst-ex-vars (with-current-buffer proof-shell-buffer (funcall proof-tree-extract-instantiated-existentials |