From ecb47478c9f9959ea25ce509076f6e3959d2c620 Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Thu, 14 May 2020 15:29:58 +0200
Subject: All case for Show and regex variable

---
 generic/proof-config.el | 5 +++++
 generic/proof-shell.el  | 7 +++++--
 2 files changed, 10 insertions(+), 2 deletions(-)

(limited to 'generic')

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)))))
-- 
cgit v1.2.3