coq: fix goals update after error

This commit fixes two more cases of ProofGeneral#568: The goals buffer is updated
in case of an error if Coq is inside a proof. Care is taken to keep
the error message in the response buffer and to show the response
buffer in two-pane mode.

The fix works by issuing a Show command as a priority action item from
proof-shell-handle-error-or-interrupt-hook, which runs at the end of
the error processing. The new action item flag 'keep-response tells
the generic machinery to not clear the response buffer and to keep it
in two-pane mode.

Author: hendriktews

ci/simple-tests/coq-test-goals-present.el

@@ -251,7 +251,6 @@ which action the goals buffer should have been reset."
 
 (ert-deftest goals-after-error ()
   "Test goals are present after an error."
-  :expected-result :failed
   (goals-after-test coq-src-error "error" t))
 
 (ert-deftest goals-reset-after-admitted ()
@@ -272,7 +271,6 @@ which action the goals buffer should have been reset."
 
 (ert-deftest update-goals-after-error ()
   "Test goals are updated after an error."
-  :expected-result :failed
   (message "update-goals-after-error: Check goals are updated after error")
   (setq proof-three-window-enable nil)
   (let (buffer)

coq/coq.el

@@ -133,7 +133,7 @@ buffer.
 
 Sets silent mode.
 
-In normal interaction, the Coq is started because the user assert
+In normal interaction, Coq is started because the user assert
 some commands. Therefore the commands here are followed by those
 inserted inside `proof-assert-command-hook', respectively,
 `coq-adapt-printing-width'.")
@@ -1874,7 +1874,7 @@ at `proof-assistant-settings-cmds' evaluation time.")
           (let ((pt2 (point)))
             (re-search-backward "Goal:\\|^TcDebug\\|^</prompt>" nil t)
             (when (looking-at "Goal")
-              (pg-goals-display (buffer-substring (point) pt2) nil))))))))
+              (pg-goals-display (buffer-substring (point) pt2) nil nil))))))))
 
 ;; overwrite the generic one, interactive prompt is Debug mode;; try to display
 ;; the debug goal in the goals buffer.
@@ -3063,6 +3063,26 @@ buffer."
 (add-hook 'proof-shell-handle-error-or-interrupt-hook #'coq-highlight-error-hook t)
 
 
+(defun coq-show-goals-on-error ()
+  "Update goals buffer on error if necessary.
+This function is intended for
+`proof-shell-handle-error-or-interrupt-hook'. When Coq reported
+an error, this function issues a Show command to update the goals
+buffer, in case we are inside a proof. The hook is processed deep
+inside `proof-shell-filter' after the action list has been reset
+and the proof shell lock `proof-shell-busy' has been released,
+all because of the error. The Show must therefore be added as
+priority action. The flags of the action item must contain
+`'keep-response', because in two-pane mode we want to show the
+response buffer to the user."
+  (when coq-last-but-one-proofstack
+    (proof-add-to-priority-queue
+     (proof-shell-action-list-item
+      "Show. " 'proof-done-invisible
+      (list 'keep-response 'invisible 'empty-action-list)))))
+
+(add-hook 'proof-shell-handle-error-or-interrupt-hook #'coq-show-goals-on-error)
+
 ;;
 ;; Scroll response buffer to maximize display of first goal
 ;;

doc/PG-adapting.texi

@@ -3888,6 +3888,7 @@ bother the user.  They may include
   @code{'no-response-display}      do not display messages in @strong{response} buffer
   @code{'no-error-display}         do not display errors/take error action
   @code{'no-goals-display}         do not goals in @strong{goals} buffer
+  @code{'keep-response}            do not erase the response buffer when goals are shown
   @code{'proof-tree-show-subgoal}  item inserted by the proof-tree package
   @code{'priority-action}          item added via @code{proof-add-to-priority-queue}
   @code{'empty-action-list}        @code{proof-shell-empty-action-list-command} should not be

generic/pg-goals.el

@@ -79,7 +79,7 @@ May enable proof-by-pointing or similar features.
 ;;
 ;; Goals buffer processing
 ;;
-(defun pg-goals-display (string keepresponse)
+(defun pg-goals-display (string keepresponse nodisplay)
   "Display STRING in the `proof-goals-buffer', properly marked up.
 Converts term substructure markup into mouse-highlighted extents.
 
@@ -90,7 +90,13 @@ function tries to do that by calling `pg-response-maybe-erase'.
 If KEEPRESPONSE is non-nil, we assume that a response message
 corresponding to this goals message has already been displayed
 before this goals message (see `proof-shell-handle-delayed-output'),
-so the response buffer should not be cleared."
+so the response buffer should not be cleared.
+
+IF NODISPLAY is non-nil, do not display the goals buffer in some
+window (but the goals buffer is updated as described above and
+any window currently showing it will keep it). In two-pane mode,
+NODISPLAY has the effect that the goals are updated but the
+response buffer is displayed."
   ;; Response buffer may be out of date. It may contain (error)
   ;; messages relating to earlier proof states
 
@@ -114,8 +120,11 @@ so the response buffer should not be cleared."
     (set-buffer-modified-p nil)
 
     ;; Keep point at the start of the buffer.
-    (proof-display-and-keep-buffer
-     proof-goals-buffer (point-min))))
+    ;; (For Coq, somebody sets point to the conclusion in the goal, so the
+    ;; position argument in proof-display-and-keep-buffer has no effect.)
+    (unless nodisplay
+      (proof-display-and-keep-buffer
+       proof-goals-buffer (point-min)))))
 
 ;;
 ;; Actions in the goals buffer

generic/proof-shell.el

@@ -38,6 +38,8 @@
 ;;         -> proof-shell-process-urgent-message
 ;;      -> proof-shell-filter-manage-output
 ;;         -> proof-shell-handle-immediate-output
+;;            -> proof-shell-handle-error-or-interrupt
+;;               -> proof-shell-error-or-interrupt-action
 ;;         -> proof-shell-exec-loop
 ;;            -> proof-tree-check-proof-finish
 ;;            -> proof-shell-handle-error-or-interrupt
@@ -113,6 +115,7 @@ bother the user.  They may include
   'no-response-display      do not display messages in *response* buffer
   'no-error-display         do not display errors/take error action
   'no-goals-display         do not goals in *goals* buffer
+  'keep-response            do not erase the response buffer when goals are shown
   'proof-tree-show-subgoal  item inserted by the proof-tree package
   'priority-action          item added via proof-add-to-priority-queue
   'empty-action-list        proof-shell-empty-action-list-command should not be
@@ -1818,7 +1821,9 @@ i.e., 'goals or 'response."
 	    (buffer-substring-no-properties rstart gmark)))
        ;; display goals output second so it persists in 2-pane mode
        (unless (memq 'no-goals-display flags)
-	 (pg-goals-display proof-shell-last-goals-output both))
+	 (pg-goals-display proof-shell-last-goals-output
+                           (or both (member 'keep-response flags))
+                           (member 'keep-response flags)))
        ;; indicate a goals output has been given
        'goals))