From 8e12eee54e36ca16d4b4530e1509479f22929e4f Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Mon, 11 May 2020 15:00:47 +0200
Subject: First try for feature #487

---
 coq/coq-abbrev.el         |  9 +++++++--
 coq/coq-compile-common.el | 10 ++++++++++
 coq/coq-showdiff.el       | 12 ++++++++++++
 coq/coq.el                |  9 ++++++++-
 4 files changed, 37 insertions(+), 3 deletions(-)
 create mode 100644 coq/coq-showdiff.el

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index bd898a9c..4d2c8287 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-toggle
+      :style toggle
+      :selected coq-show-proof
+      :help "Show the proof diffs 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..2a5c3f44 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -458,6 +458,16 @@ This option can be set via menu
 ;; define coq-lock-ancestors-toggle
 (proof-deftoggle coq-lock-ancestors)
 
+;; Maybe not the good place
+(defcustom coq-show-proof nil
+  "TODO: doc"
+
+  :type 'boolean
+  :safe 'booleanp
+  :group 'coq-auto-compile)
+
+(proof-deftoggle coq-show-proof)
+
 (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-showdiff.el b/coq/coq-showdiff.el
new file mode 100644
index 00000000..f42431af
--- /dev/null
+++ b/coq/coq-showdiff.el
@@ -0,0 +1,12 @@
+;; Temporary file, just for test
+(defun coq-show-proof-fun ()
+  (interactive)
+  ;; TODO: Check if we are in a proof
+  (when coq-show-proof
+    (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.el b/coq/coq.el
index 71112fc1..8ebf3054 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1222,7 +1222,14 @@ be called and no command will be sent to Coq."
      (string-match-p "BackTo\\s-" cmd))
     (if (coq--post-v810)
         (list "Unset Silent." (coq-diffs))
-      (list "Unset Silent.")))))
+      (list "Unset Silent.")))
+   ((or
+     ;; 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
+            (list  "Show Proof." "Show.")))))))
+
 
 (defpacustom auto-adapt-printing-width t
   "If non-nil, adapt automatically printing width of goals window.
-- 
cgit v1.2.3