coq: clear goals buffer after admitted

Only add the declaration info message to the right regular expression
and generic Proof General will clear the goals buffer. As a side
effect the declaration info message won't show up in the response
buffer any more. Need to change the tests that rely on this.

Author: hendriktews

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

@@ -174,7 +174,6 @@ goals buffer is not empty afterwards."
   (goals-after-test coq-src-error "error"))
 
 (ert-deftest goals-reset-after-admitted ()
-  :expected-result :failed
   "The goals buffer is reset after an Admitted."
   (message
    "goals-reset-after-admitted: Check that goals are reset after Admitted.")

ci/simple-tests/coq-test-omit-proofs.el

@@ -92,10 +92,11 @@ configured there may be taken from faces with less priority."
   "Test the omit proofs feature.
 In particular, test that with proof-omit-proofs-option configured:
 - the proof _is_ processed when using a prefix argument
-- in this case the proof as normal locked color
+- in this case the proof has normal locked color
 - without prefix arg, the proof is omitted
 - the proof has omitted color then
 - stuff before the proof still has normal color "
+  (message "omit-proofs-omit-and-not-omit: Check several omit proofs features")
   (setq proof-omit-proofs-option t
         proof-three-window-enable nil)
   (reset-coq)
@@ -154,10 +155,21 @@ In particular, test that with proof-omit-proofs-option configured:
   (forward-line -1)
   (proof-goto-point)
   (wait-for-coq)
-  (with-current-buffer "*response*"
-    (goto-char (point-min))
-    ;; There should be a declared message.
-    (should (looking-at "classic_excluded_middle is declared")))
+  (with-current-buffer "*coq*"
+    ;; There should be an Admit at the second last prompt without error.
+    (goto-char (point-max))
+    (should (search-backward "</prompt>" nil t 2))
+    ;; move behind prompt
+    (forward-char 9)
+    (should (looking-at "Admitted\\.\n"))
+    (forward-line 1)
+    ;; There may be an info message about the declaration. The message
+    ;; may be spread over several lines.
+    (when (looking-at "<infomsg>")
+      (should (search-forward "</infomsg>" nil t))
+      (forward-line 1))
+    ;; no other messages or errors before the next prompt
+    (should (looking-at "\n<prompt>Coq <")))
 
   ;; Check 4: check proof-omitted-proof-face is active at marker 3
   (message "4: check proof-omitted-proof-face is active at marker 3")
@@ -184,6 +196,7 @@ the normal `proof-locked-face'.
 
 The sources for the test contain a local attribute in form of
 '#[local]', which has been introduced only in Coq version 8.9."
+  (message "omit-proofs-never-omit-hints: Check omit proofs feature with Hint")
   (skip-unless coq--post-v809)
   (setq proof-omit-proofs-option t
         proof-three-window-enable nil)
@@ -206,6 +219,7 @@ Test that proofs for Let local declarations are never omitted and
 that proofs of theorems following a Let definition are omitted.
 
 This test only checks the faces in the middle of the proof."
+  (message "omit-proofs-never-omit-lets: Check omit proofs feature with Let")
   (setq proof-omit-proofs-option t
         proof-three-window-enable nil)
   (reset-coq)

coq/coq.el

@@ -145,8 +145,20 @@ Namely, goals that do not fit in the goals window."
 ;;  "Add LoadPath \"%s\"." ;; fixes unadorned Require (if .vo exists).
   "*Command of the inferior process to change the directory.")
 
-(defvar coq-shell-proof-completed-regexp "No\\s-+more\\s-+\\(?:sub\\)?goals\\.\\|Subtree\\s-proved!\\|Proof\\s-completed"; \\|This subproof is complete
-  "*Regular expression indicating that the proof has been completed.")
+(defvar coq-shell-proof-completed-regexp
+  (concat "No\\s-+more\\s-+\\(?:sub\\)?goals\\.\\|Subtree\\s-proved!\\|"
+          "Proof\\s-completed\\|"
+          ;; if printing width is small, eg. when running in batch mode,
+          ;; there might be a line break after infomsg
+          "<infomsg>\n?.*\\s-is\\s-declared"
+          ;; \\|This subproof is complete
+          )
+  "*Regular expression indicating that the proof has been completed.
+Coq instance of `proof-shell-clear-goals-regexp'. Used in
+`proof-shell-process-urgent-message' to determine if the goals
+buffer shall be cleaned. Some of the messages recognized here are
+not printed by Coq in silent mode, such that Proof General might
+fail to delete the goals buffer.")
 
 (defvar coq-goal-regexp
   "\\(============================\\)\\|\\(\\(?:sub\\)?goal [0-9]+\\)\n")

generic/proof-shell.el

@@ -35,6 +35,7 @@
 ;;   proof-shell-filter-wrapper
 ;;   -> proof-shell-filter
 ;;      -> proof-shell-process-urgent-messages
+;;         -> proof-shell-process-urgent-message
 ;;      -> proof-shell-filter-manage-output
 ;;         -> proof-shell-handle-immediate-output
 ;;         -> proof-shell-exec-loop