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

ci/coq-tests.el

@@ -66,7 +66,7 @@
 
 (defun coq-test-exit ()
   "Exit the Coq process."
-  (proof-shell-exit t)) 
+  (proof-shell-exit t))
 
 ; (coq-test-on-file nil (message (buffer-file-name)) (message "OK") 42)
 
@@ -110,8 +110,11 @@
    #'proof-done-invisible
    'no-error-display 'no-response-display 'no-goals-display))
 
+(defun coq-set-flags (val flags)
+  (when (member 'show-proof-stepwise flags) (setq coq-show-proof-stepwise val))
+  (when (member 'diffs-on flags) (if val (setq coq-diffs 'on) (setq coq-diffs 'off))))
 
-(defun coq-fixture-on-file (file body)
+(defun coq-fixture-on-file (file body &rest flags)
   "Fixture to setup the test env: open FILE if non-nil, or a temp file
 then evaluate the BODY function and finally tear-down (exit Coq)."
 ;; AVOID THE FOLLOWING ERROR:
@@ -142,8 +145,10 @@ then evaluate the BODY function and finally tear-down (exit Coq)."
             (with-current-buffer buffer
               (setq proof-splash-enable nil)
               (normal-mode) ;; or (coq-mode)
+	      (coq-set-flags t flags)
               (coq-mock body))))
       (coq-test-exit)
+      (coq-set-flags nil flags)
       (not-modified nil) ; Clear modification  
       (kill-buffer buffer) 
       (when rmfile (message "Removing file %s ..." rmfile))
@@ -160,11 +165,17 @@ For example, COMMENT could be (*test-definition*)"
   (goto-char (point-min))
   (search-forward comment))
 
-(defun coq-should-response (message)
-  (should (equal message
-		 (string-trim
-                  (with-current-buffer "*response*"
-                    (buffer-substring-no-properties (point-min) (point-max)))))))
+(defun coq-should-buffer-regexp (regexp &optional buffer-name)
+  "Check REGEXP matches in BUFFER-NAME (*response* if nil)."
+  (should (string-match-p
+	   regexp
+	   (string-trim
+	    (with-current-buffer (or buffer-name "*response*")
+	    (buffer-substring-no-properties (point-min) (point-max)))))))
+
+(defun coq-should-buffer-string (str &optional buffer-name)
+  "Particular case of `coq-should-buffer-regexp'."
+  (coq-should-buffer-regexp (regexp-quote str) buffer-name))
 
 ;; TODO: Use https://github.com/rejeep/ert-async.el
 ;; and/or ERT https://www.gnu.org/software/emacs/manual/html_node/ert/index.html
@@ -186,7 +197,18 @@ For example, COMMENT could be (*test-definition*)"
      (coq-test-goto-before "(*test-definition*)")
      (proof-goto-point)
      (proof-shell-wait)
-     (coq-should-response "trois is defined"))))
+     (coq-should-buffer-string "trois is defined"))))
+
+
+(ert-deftest 021_coq-test-regression-goto-point ()
+  "Regression test for proof-goto-point after a comment, PR #490"
+  (coq-fixture-on-file
+   (coq-test-full-path "test_stepwise.v")
+   (lambda ()
+       (coq-test-goto-after "(*test-definition*)")
+       (proof-goto-point)
+       (proof-shell-wait)
+       t)))
 
 
 (ert-deftest 030_coq-test-position ()
@@ -226,7 +248,7 @@ For example, COMMENT could be (*test-definition*)"
      (let ((proof-point (save-excursion (coq-test-goto-after "(*error*)")))) 
      (proof-goto-point)
      (proof-shell-wait)
-     (coq-should-response "Error: Unable to unify \"false\" with \"true\".")
+     (coq-should-buffer-string "Error: Unable to unify \"false\" with \"true\".")
      (should (equal (proof-queue-or-locked-end) proof-point))))))
 
 
@@ -254,4 +276,33 @@ For example, COMMENT could be (*test-definition*)"
      (insert "(*.*)")
      (should (equal (proof-queue-or-locked-end) 1)))))
 
+(ert-deftest 080_coq-test-regression-show-proof-stepwise()
+  "Regression test for the \"Show Proof\" option"
+  (coq-fixture-on-file
+   (coq-test-full-path "test_stepwise.v")
+   (lambda ()
+     (coq-test-goto-before " (*test-insert*)")
+     (proof-goto-point)
+     (proof-shell-wait)
+     (coq-should-buffer-string "(fun (A : Prop) (proof_of_A : A) => ?Goal)"))
+   'show-proof-stepwise))
+
+
+(ert-deftest 081_coq-test-regression-show-proof-diffs()
+  "Test for Show Proof Diffs"
+  (coq-fixture-on-file
+   (coq-test-full-path "test_stepwise.v")
+   (lambda ()
+     (coq-test-goto-before " (*test-insert*)")
+     (proof-goto-point)
+     (proof-shell-wait)
+     ;; If coq--post-v811, it should be "Show Proof Diffs." otherwise "Show Proof."
+     (if (coq--post-v811)
+	 (coq-should-buffer-string "<diff.added.bg>(fun <diff.added>(</diff.added>A : Prop<diff.added>) (proof_of_A : A)</diff.added> => ?Goal)</diff.added.bg>" "*coq*")
+       (coq-should-buffer-string "(fun (A : Prop) (proof_of_A : A) => ?Goal)")))
+   'show-proof-stepwise 'diffs-on))
+
+
+(provide 'coq-tests)
+
 ;;; coq-tests.el ends here

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)

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.

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-+\\)*\\_<"

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?

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-proof-diffs-regexp nil
+  "Matches all \"Show Proof\" forms (specific to the Coq prover)." 
+  :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

generic/proof-shell.el

@@ -1139,12 +1139,12 @@ contains only invisible elements for Prooftree synchronization."
                    (not (memq 'empty-action-list flags))
                    proof-shell-empty-action-list-command)
           (let* ((cmd (mapconcat 'identity (nth 1 item) " "))
-                (extra-cmds (apply proof-shell-empty-action-list-command (list cmd)))
-                ;; tag all new items with 'empty-action-list
-                (extra-items (mapcar (lambda (s) (proof-shell-action-list-item
-                                                  s 'proof-done-invisible
-                                                  (list 'invisible 'empty-action-list)))
-                                     extra-cmds)))
+                 (extra-cmds (apply proof-shell-empty-action-list-command (list cmd)))
+                 ;; tag all new items with 'empty-action-list
+                 (extra-items (mapcar (lambda (s) (proof-shell-action-list-item
+                                                   s 'proof-done-invisible
+                                                   (list 'invisible 'empty-action-list)))
+                                      extra-cmds)))
             ;; action-list should be empty at this point
             (setq proof-action-list (append extra-items proof-action-list))))
 
@@ -1189,11 +1189,14 @@ contains only invisible elements for Prooftree synchronization."
 	    (pg-processing-complete-hint))
 	  (pg-finish-tracing-display))
 
-	(and (not proof-second-action-list-active)
-	     (or (null proof-action-list)
-		 (cl-every
-		  (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item)))
-		  proof-action-list)))))))
+	(and (not proof-second-action-list-active) 
+	     (let ((last-command  (car (nth 1 (car (last proof-action-list))))))
+	       (or (null proof-action-list)
+	 	   (cl-every
+	 	    (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item)))
+	 	    proof-action-list)
+	 	   ;; If the last command in proof-action-list is a "Show Proof" form then return t
+	 	   (when last-command (string-match-p proof-show-proof-diffs-regexp last-command)))))))))
 
 
 (defun proof-shell-insert-loopback-cmd  (cmd)