diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-abbrev.el | 9 | ||||
| -rw-r--r-- | coq/coq-compile-common.el | 2 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 3 | ||||
| -rw-r--r-- | coq/coq.el | 61 |
4 files changed, 67 insertions, 8 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index bd898a9c..74ddb076 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -78,7 +78,7 @@ ;; Common part (script, response and goals buffers) (defconst coq-menu-common-entries `( - ["Toggle 3 Windows Mode" proof-three-window-toggle + ["Toggle 3 Windows Mode" proof-three-window-toggle :style toggle :selected proof-three-window-enable :help "Toggles the use of separate windows or frames for Coq responses and goals." @@ -243,7 +243,7 @@ :active (and coq-compile-before-require coq-compile-parallel-in-background) :help "Abort background compilation and kill all compilation processes."]) - ("Diffs" + ("Diffs" ["off" (customize-set-variable 'coq-diffs 'off) :style radio @@ -259,6 +259,11 @@ :style radio :selected (eq coq-diffs 'removed) :help "Show diffs: added and removed"]) + ["Show Proof (Diffs)" + coq-show-proof-stepwise-toggle + :style toggle + :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 f9a3571e..938f706e 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -458,6 +458,8 @@ This option can be set via menu ;; define coq-lock-ancestors-toggle (proof-deftoggle coq-lock-ancestors) +(proof-deftoggle coq-show-proof-stepwise) + (defcustom coq-confirm-external-compilation t "If set let user change and confirm the compilation command. Otherwise start the external compilation without confirmation. diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 470331a6..5b8d8c48 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1304,6 +1304,9 @@ It is used: "*Font-lock table for Coq terms.") +(defconst coq-show-proof-diffs-regexp + "\\`Show Proof\\(?: Diffs\\| Diffs removed\\)?\\.\\'") + (defconst coq-save-command-regexp ;; FIXME: The surrounding grouping parens are probably not needed. (concat "\\`\\(\\(?:Time\\s-+\\|Timeout\\s-+[[:digit:]]+\\s-+\\)*\\_<" @@ -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 ;; @@ -1199,7 +1209,9 @@ Printing All set." "Return the list of commands to send to Coq after CMD if it is the last command of the action list. If CMD is tagged with 'empty-action-list then this function won't -be called and no command will be sent to Coq." +be called and no command will be sent to Coq. +Note: the last command added if `coq-show-proof-stepwise' is set +should match the `coq-show-proof-diffs-regexp'." (cond ((or ;; If closing a nested proof, Show the enclosing goal. @@ -1208,21 +1220,56 @@ 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))) - (list "Show.")) + (let ((showlist (list "Show."))) + (when coq-show-proof-stepwise + (add-to-list 'showlist + (if (coq--post-v811) + (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.")) + "Show Proof.") + t)) + showlist)) + ((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) "Show."))) + (let ((showlist (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")))) + (when coq-show-proof-stepwise + (add-to-list 'showlist + (if (coq--post-v811) + (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.")) + "Show Proof.") + t)) + showlist)) + ((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."))))) + (list "Unset Silent." (coq-diffs) ) + (list "Unset Silent."))) + ((or + ;; If starting a proof, Show Proof if need be + (coq-goal-command-str-p cmd) + ;; 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 + (if (coq--post-v811) + (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."))) + (list "Show Proof.")))))) + (defpacustom auto-adapt-printing-width t "If non-nil, adapt automatically printing width of goals window. @@ -1890,6 +1937,8 @@ at `proof-assistant-settings-cmds' evaluation time.") proof-save-command "Save %s. " proof-find-theorems-command "Search %s. ") + (setq proof-show-proof-diffs-regexp coq-show-proof-diffs-regexp) + (setq proof-shell-empty-action-list-command 'coq-empty-action-list-command) ;; FIXME da: Does Coq have a help or about command? |