diff options
| -rw-r--r-- | coq/coq-abbrev.el | 8 | ||||
| -rw-r--r-- | coq/coq-compile-common.el | 4 | ||||
| -rw-r--r-- | coq/coq-showdiff.el | 4 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 3 | ||||
| -rw-r--r-- | coq/coq.el | 8 | ||||
| -rw-r--r-- | generic/proof-config.el | 2 |
6 files changed, 15 insertions, 14 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 4d2c8287..74ddb076 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -259,11 +259,11 @@ :style radio :selected (eq coq-diffs 'removed) :help "Show diffs: added and removed"]) - ["Show proof diffs" - coq-show-proof-toggle + ["Show Proof (Diffs)" + coq-show-proof-stepwise-toggle :style toggle - :selected coq-show-proof - :help "Show the proof diffs in the response buffer"] + :selected coq-show-proof-stepwise + :help "Display the proof terms stepwise in the *response* buffer."] ("\"Proof using\" mode..." ["ask" (customize-set-variable 'coq-accept-proof-using-suggestion 'ask) diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 2a5c3f44..fdb3d4b8 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -459,14 +459,14 @@ This option can be set via menu (proof-deftoggle coq-lock-ancestors) ;; Maybe not the good place -(defcustom coq-show-proof nil +(defcustom coq-show-proof-stepwise nil "TODO: doc" :type 'boolean :safe 'booleanp :group 'coq-auto-compile) -(proof-deftoggle coq-show-proof) +(proof-deftoggle coq-show-proof-stepwise) (defcustom coq-confirm-external-compilation t "If set let user change and confirm the compilation command. diff --git a/coq/coq-showdiff.el b/coq/coq-showdiff.el index f42431af..0daf98f8 100644 --- a/coq/coq-showdiff.el +++ b/coq/coq-showdiff.el @@ -2,11 +2,11 @@ (defun coq-show-proof-fun () (interactive) ;; TODO: Check if we are in a proof - (when coq-show-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."))) - )
\ No newline at end of file + ) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index e486997d..a27274c5 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1304,7 +1304,8 @@ It is used: "*Font-lock table for Coq terms.") -(defconst coq-show-diffs-regexp +(defconst coq-show-proof-diffs-regexp + ;; FIXME/TODO: enhance this regexp "Show Proof\\(\\.\\| Diffs\\.\\| Diffs removed\\.\\)") (defconst coq-save-command-regexp @@ -1208,7 +1208,7 @@ 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 + (if coq-show-proof-stepwise (or (when (eq coq-diffs 'off) (list "Show." "Show Proof." )) (when (eq coq-diffs 'on) (list "Show." "Show Proof Diffs.")) @@ -1221,7 +1221,7 @@ be called and no command will be sent to Coq." (> (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 + (if coq-show-proof-stepwise ((when (eq coq-diffs 'off) "Show." "Show Proof." ) (when (eq coq-diffs 'on) @@ -1240,7 +1240,7 @@ be called and no command will be sent to Coq." ;; 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 + (when coq-show-proof-stepwise (list "Show." "Show Proof."))))))) @@ -1910,7 +1910,7 @@ at `proof-assistant-settings-cmds' evaluation time.") proof-save-command "Save %s. " proof-find-theorems-command "Search %s. ") - (setq proof-show-diffs-regexp coq-show-diffs-regexp) + (setq proof-show-proof-diffs-regexp coq-show-proof-diffs-regexp) (setq proof-shell-empty-action-list-command 'coq-empty-action-list-command) diff --git a/generic/proof-config.el b/generic/proof-config.el index 16cdae93..ce72c76c 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -399,7 +399,7 @@ NB: This setting is not used for matching output from the prover." :type 'regexp :group 'proof-script) -(defcustom proof-show-diffs-regexp nil +(defcustom proof-show-proof-diffs-regexp nil "Matches all Show Proof form" :type 'regexp :group 'proof-script) |