Merge pull request #490 from ProofGeneral/feature/487

Improve PG support of Show Proof (Diffs):
Display the proof terms stepwise in the *response* buffer.
Close #487

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-+\\)*\\_<"
diff --git a/coq/coq.el b/coq/coq.el
index 71112fc1..efa60349 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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?