diff options
| -rw-r--r-- | coq/coq-compile-common.el | 8 | ||||
| -rw-r--r-- | coq/coq-showdiff.el | 12 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 2 | ||||
| -rw-r--r-- | coq/coq.el | 44 | ||||
| -rw-r--r-- | generic/proof-config.el | 2 | ||||
| -rw-r--r-- | generic/proof-shell.el | 14 |
6 files changed, 36 insertions, 46 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index fdb3d4b8..938f706e 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -458,14 +458,6 @@ This option can be set via menu ;; define coq-lock-ancestors-toggle (proof-deftoggle coq-lock-ancestors) -;; Maybe not the good place -(defcustom coq-show-proof-stepwise nil - "TODO: doc" - - :type 'boolean - :safe 'booleanp - :group 'coq-auto-compile) - (proof-deftoggle coq-show-proof-stepwise) (defcustom coq-confirm-external-compilation t diff --git a/coq/coq-showdiff.el b/coq/coq-showdiff.el deleted file mode 100644 index 0daf98f8..00000000 --- a/coq/coq-showdiff.el +++ /dev/null @@ -1,12 +0,0 @@ -;; Temporary file, just for test -(defun coq-show-proof-fun () - (interactive) - ;; TODO: Check if we are in a proof - (when coq-show-proof-stepwise - (when (eq coq-diffs 'off) - (proof-shell-invisible-command "Show Proof." )) - (when (eq coq-diffs 'on) - (proof-shell-invisible-command "Show Proof Diffs.")) - (when (eq coq-diffs 'removed) - (proof-shell-invisible-command "Show Proof Diffs removed."))) - ) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 3ae7fbca..47869aed 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1305,7 +1305,7 @@ It is used: (defconst coq-show-proof-diffs-regexp - "^[ ]*Show Proof\\( Diffs\\| Diffs removed\\)?\\.$") + "\\bShow Proof\\(?: Diffs\\| Diffs removed\\)?\\.\\b") (defconst coq-save-command-regexp ;; FIXME: The surrounding grouping parens are probably not needed. @@ -160,6 +160,16 @@ See also option `coq-hide-additional-subgoals'." :type '(choice regexp (const nil)) :group 'coq) +(defcustom coq-show-proof-stepwise nil + "Display the proof terms stepwise in the *response* buffer. + This option can be combined with option `coq-diffs'. + It is mostly useful in three window mode, see also + `proof-three-window-mode-policy' for details." + + :type 'boolean + :safe 'booleanp + :group 'coq-auto-compile) + ;; ;; prooftree customization ;; @@ -1208,40 +1218,42 @@ be called and no command will be sent to Coq." ;; If user issued a printing option then t printing. (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd) (> (length coq-last-but-one-proofstack) 0))) - (if coq-show-proof-stepwise + (list "Show." + (when coq-show-proof-stepwise (or - (when (eq coq-diffs 'off) (list "Show." "Show Proof." )) - (when (eq coq-diffs 'on) (list "Show." "Show Proof Diffs.")) - (when (eq coq-diffs 'removed) (list "Show." "Show Proof Diffs removed."))) - (list "Show."))) + (when (eq coq-diffs 'off) "Show Proof.") + (when (eq coq-diffs 'on) "Show Proof Diffs.") + (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) + ((or ;; If we go back in the buffer and the number of abort is less than ;; the number of nested goals, then Unset Silent and Show the goal (and (string-match-p "BackTo\\s-" cmd) (> (length coq-last-but-one-proofstack) coq--retract-naborts))) ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs - (list "Unset Silent." (if (coq--post-v810) (coq-diffs) - (if coq-show-proof-stepwise - ((when (eq coq-diffs 'off) - "Show." "Show Proof." ) - (when (eq coq-diffs 'on) - "Show." "Show Proof Diffs.") - (when (eq coq-diffs 'removed) - "Show." "Show Proof Diffs removed.")) - "Show.")))) + (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.") + (when coq-show-proof-stepwise + (or + (when (eq coq-diffs 'off) "Show Proof.") + (when (eq coq-diffs 'on) "Show Proof Diffs.") + (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) + ((or ;; If we go back in the buffer and not in the above case, then only Unset ;; silent (there is no goal to show). Still, we need to "Set Diffs" again (string-match-p "BackTo\\s-" cmd)) (if (coq--post-v810) - (list "Unset Silent." (coq-diffs)) + (list "Unset Silent." (coq-diffs) ) (list "Unset Silent."))) ((or ;; If doing (not closing) a proof, Show Proof if need be (and (not (string-match-p coq-save-command-regexp-strict cmd)) (> (length coq-last-but-one-proofstack) 0) (when coq-show-proof-stepwise - (list "Show." "Show Proof."))))))) + (or + (when (eq coq-diffs 'off) (list "Show Proof." )) + (when (eq coq-diffs 'on) (list "Show Proof Diffs.")) + (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed."))))))))) (defpacustom auto-adapt-printing-width t diff --git a/generic/proof-config.el b/generic/proof-config.el index ce72c76c..9d352548 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -400,7 +400,7 @@ NB: This setting is not used for matching output from the prover." :group 'proof-script) (defcustom proof-show-proof-diffs-regexp nil - "Matches all Show Proof form" + "Matches all \"Show Proof\" forms (specific to the Coq prover)." :type 'regexp :group 'proof-script) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 8f23608a..1258c7f6 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1126,7 +1126,7 @@ contains only invisible elements for Prooftree synchronization." ;; but we delay this until sending the next command, attempting ;; to parallelize prover and Emacs somewhat. (PG 4.0 change) - (setq proof-action-list (cdr proof-action-list)) + (setq proof-action-list (cdr proof-action-list)) (setq cbitems (cons item (proof-shell-slurp-comments))) @@ -1194,7 +1194,8 @@ contains only invisible elements for Prooftree synchronization." (cl-every (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) proof-action-list) - (string= (car (nth 1 item)) "Show."))))))) + ;; If the last command in proof-action-list is a "Show Proof" form then return t + (string-match-p proof-show-proof-diffs-regexp (car (nth 1 (car (last proof-action-list))))))))))) (defun proof-shell-insert-loopback-cmd (cmd) @@ -1616,12 +1617,9 @@ by the filter is to send the next command from the queue." (setq proof-shell-delayed-output-end end) (setq proof-shell-delayed-output-flags flags) (if (proof-shell-exec-loop) - ;; (if (and (string-match proof-show-diffs-regexp (car cmd)) - ;; (memq 'empty-action-list flags)) - ;; (setq proof-shell-last-output-kind 'response) + (setq proof-shell-last-output-kind ;; only display result for last output - (setq proof-shell-last-output-kind (proof-shell-handle-delayed-output))) - ;; + (proof-shell-handle-delayed-output))) ;; send output to the proof tree visualizer (if proof-tree-external-display (proof-tree-handle-delayed-output old-proof-marker cmd flags span))))) @@ -1716,7 +1714,7 @@ i.e., 'goals or 'response." (buffer-substring-no-properties rstart gmark))) ;; display goals output second so it persists in 2-pane mode (unless (memq 'no-goals-display flags) - (pg-goals-display proof-shell-last-goals-output t)) + (pg-goals-display proof-shell-last-goals-output both)) ;; indicate a goals output has been given 'goals)) |