All case for Show and regex variable

4 files changed, 31 insertions, 5 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 470331a6..e486997d 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-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 8ebf3054..65ff488f 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1208,14 +1208,27 @@ 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."))
+    (if coq-show-proof
+        (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.")))
    ((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.")))
+    (list "Unset Silent." (if (coq--post-v810) (coq-diffs)
+                            (if coq-show-proof
+    ((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."))))
    ((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
@@ -1228,7 +1241,7 @@ be called and no command will be sent to Coq."
      (and (not (string-match-p coq-save-command-regexp-strict cmd))
           (> (length coq-last-but-one-proofstack) 0)
           (when coq-show-proof
-            (list  "Show Proof." "Show.")))))))
+            (list "Show." "Show Proof.")))))))
 
 
 (defpacustom auto-adapt-printing-width t
@@ -1897,6 +1910,8 @@ 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-shell-empty-action-list-command 'coq-empty-action-list-command)
 
 ;; FIXME da: Does Coq have a help or about command?
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 8d539191..16cdae93 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -399,6 +399,11 @@ NB: This setting is not used for matching output from the prover."
   :type 'regexp
   :group 'proof-script)
 
+(defcustom proof-show-diffs-regexp nil
+  "Matches all Show Proof form"
+  :type 'regexp
+  :group 'proof-script)
+
 (defcustom proof-save-with-hole-regexp nil
   "Regexp which matches a command to save a named theorem.
 The name of the theorem is built from the variable
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index a0e80fa7..b6bf9225 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1615,9 +1615,12 @@ 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)
-	  (setq proof-shell-last-output-kind
+	  ;; (if (and  (string-match proof-show-diffs-regexp (car cmd))
+	  ;; 		  (memq 'empty-action-list flags))
+	  ;; (setq proof-shell-last-output-kind 'response)
 		;; only display result for last output
-		(proof-shell-handle-delayed-output)))
+	  (setq proof-shell-last-output-kind (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)))))