experiment for #188 and #429 -- insert show after error in silent mode

coq/coq.el

@@ -661,7 +661,7 @@ If locked span already has a state number, then do nothing. Also updates
 ;; This hook seems the one we want.
 ;; WARNING! It is applied once after each command PLUS once before a group of
 ;; commands is started
-(add-hook 'proof-state-change-hook #'coq-set-state-infos)
+(add-hook 'proof-state-change-pre-hook #'coq-set-state-infos)
 
 
 (defun count-not-intersection (l notin)

generic/proof-config.el

@@ -1771,6 +1771,15 @@ This hook is used within Proof General to refresh the toolbar."
   :type '(repeat function)
   :group 'proof-shell)
 
+
+(defcustom proof-state-change-pre-hook nil
+  "Things to do before proof-done-advancing.
+
+E.g. classify spans by looking at the prompt."
+  :type '(repeat function)
+  :group 'proof-shell)
+
+
 ;;;;;;
 (defcustom proof-dependencies-system-specific nil
   "Set this variable to handle system specific dependency output.
@@ -1787,7 +1796,6 @@ same type as `proof-dependency-in-span-context-menu' returns."
   :type '(repeat function)
   :group 'proof-shell)
 ;;;;;
-
 (defcustom proof-shell-syntax-table-entries nil
   "List of syntax table entries for proof script mode.
 A flat list of the form

generic/proof-script.el

@@ -1382,6 +1382,8 @@ Argument SPAN has just been processed."
     (if (span-live-p proof-queue-span)
 	(proof-set-queue-start end))
 
+    (run-hooks 'proof-state-change-pre-hook)
+
     (cond
      ;; CASE 1: Comments just get highlighted
      ((eq (span-property span 'type) 'comment)
@@ -2120,6 +2122,7 @@ which is true for some proof assistants (but probably not others)."
 	(span-delete span)
 	(if killfn (funcall killfn start end))))
   ;; State of scripting may have changed now
+  (run-hooks 'proof-state-change-pre-hook)
   (run-hooks 'proof-state-change-hook))
 
 (defun proof-setup-retract-action (start end proof-commands remove-action &optional

generic/proof-shell.el

@@ -92,6 +92,22 @@ printing hints).
 
 See the functions `proof-start-queue' and `proof-shell-exec-loop'.")
 
+(defvar proof-priority-action-list nil
+  "Holds action items to be inserted at the head of `proof-action-list' ASAP.
+When the proof assistant is busy, one cannot push to the head of
+`proof-action-list`, because the head usually (but not always)
+contains the item that the proof assistant is currently
+executing. This list therefore holds the items to be executed
+before any other items in `proof-action-list'. Inside
+`proof-shell-exec-loop', when `proof-action-list' is in the right
+state, the content of this list if prepended to
+`proof-action-list'. Use `proof-add-to-priority-queue' to add
+items to this priority list, to ensure the proof assistant starts
+running, in case `proof-action-list' is currently empty.
+
+The items in this list are reversed, that is, the one added last
+and to be executed last is at the head.")
+
 (defsubst proof-shell-invoke-callback (listitem)
   "From `proof-action-list' LISTITEM, invoke the callback on the span."
   (condition-case err
@@ -1062,6 +1078,32 @@ being processed."
       ;; nothing to do: maybe we completed a list of comments without sending them
 	(proof-detach-queue)))))
 
+(defun start-prover-with-priority-items-maybe ()
+  "Start processing priority items if necessary.
+If there are priority items and the proof shell is not busy with
+other items, then this function starts the prover with the
+priority items. This function relies on the invariants of
+`proof-shell-filter-active' and on `proof-action-list'. The
+latter is non-empty, if there is some item, which has not been
+fully processed yet.
+
+Note that inside `proof-shell-exec-loop' the priority items are
+processed without calling this function."
+  (when (and proof-priority-action-list
+             (null proof-action-list) (not proof-shell-filter-active))
+    ;; not sure how fast we end up in proof-shell-exec-loop, better to clear
+    ;; proof-priority-action-list here before calling proof-add-to-queue
+    (let ((copy proof-priority-action-list))
+      (setq proof-priority-action-list nil)
+      (proof-add-to-queue (nreverse copy)))))
+
+(defun proof-add-to-priority-queue (queueitem)
+  "Add item to `proof-priority-action-list' and start the queue if necessary.
+Argument QUEUEITEM must be an action item as documented for
+`proof-action-list'."
+  (push queueitem proof-priority-action-list)
+  (start-prover-with-priority-items-maybe))
+
 
 ;;;###autoload
 (defun proof-start-queue (start end queueitems &optional queuemode)
@@ -1158,6 +1200,13 @@ contains only invisible elements for Prooftree synchronization."
 	(if proof-tree-external-display
 	    (proof-tree-urgent-action flags))
 
+        ;; add priority actions to the front of proof-action-list
+        (when proof-priority-action-list
+          (setq proof-action-list
+                (nconc (nreverse proof-priority-action-list)
+                       proof-action-list))
+          (setq proof-priority-action-list nil))
+
 	;; if action list is (nearly) empty, ensure prover is noisy.
 	(if (and proof-shell-silent
 		 (not (eq (nth 2 item) 'proof-shell-clear-silent))
@@ -1387,7 +1436,7 @@ to `proof-register-possibly-new-processed-file'."
   "Wrapper for `proof-shell-filter', protecting against parallel calls.
 In Emacs a process filter function can be called while the same
 filter is currently running for the same process, for instance,
-when the filter bocks on I/O. This wrapper protects the main
+when the filter blocks on I/O. This wrapper protects the main
 entry point, `proof-shell-filter' against such parallel,
 overlapping calls.
 
@@ -1412,7 +1461,10 @@ calls."
 	   (setq proof-shell-filter-active nil
 		 proof-shell-filter-was-blocked nil)
 	   (signal (car err) (cdr err))))
-	(setq call-proof-shell-filter proof-shell-filter-was-blocked)))))
+	(setq call-proof-shell-filter proof-shell-filter-was-blocked)))
+    ;; finally leaving proof-shell-filter - maybe somebody has added
+    ;; priority items inside proof-shell-filter?
+    (start-prover-with-priority-items-maybe)))
 
 
 (defun proof-shell-filter ()
@@ -1608,8 +1660,41 @@ by the filter is to send the next command from the queue."
 	  (buffer-substring-no-properties start end))
 
     ;; sets proof-shell-last-output-kind
+    ;;; NB This will remove the span (and all following queued spans)
+    ;;; if an error occured. So don't use it in the following unless
+    ;;; you know the command was processed without error.
     (proof-shell-handle-immediate-output cmd start end flags)
 
+    ;; insert a show proof command to have an up-to-date goals buffer
+    ;; in case of error. Currently PG makes coq silent when proccesing
+    ;; a bunch of commands, and goes back to unsilent before the last
+    ;; command. Therefore if an error interrupts a bunch we are still
+    ;; in silent mode and the goal is not diplayed. The following
+    ;; inserts a show proof command to have an up-to-date goals buffer
+    ;; in case of error AND we are in a proof. We don't issue the show
+    ;; command in other cases as it would be redundant or wrong.
+
+    ;; NB: If we switch to "all silent, ask for show" protocol, then
+    ;; this would need to be generalized, but maybe not here.
+
+    ;; NB: To avoid looping on errors (like if the printing of the
+    ;; goal is not possible) these actions are tagged with the flag
+    ;; 'empty-action-list and trigger the following only if its this
+    ;; flag is missing.
+    (when (and (not (memq 'empty-action-list flags))
+               (funcall proof-shell-last-cmd-left-goals-p)
+               (eq proof-shell-last-output-kind 'error))
+      ;; to make the error message stay, we need to send a Show
+      ;; command without updating any buffer and then use the
+      ;; pg-goals-display can insert the output in goals buffer
+      ;; without changing the response buffer.
+      (let ((callback '(lambda (dummyspan);do not use the span, it is probably deleted
+                         (pg-goals-display proof-shell-last-output t))))
+        (proof-add-to-priority-queue
+         (proof-shell-action-list-item
+          proof-showproof-command callback ;'proof-done-invisible
+           (list 'no-goals-display 'invisible 'empty-action-list)))))
+
     (unless proof-shell-last-output-kind ; dealt with already
       (setq proof-shell-delayed-output-start start)
       (setq proof-shell-delayed-output-end end)
@@ -1833,6 +1918,7 @@ If TIMEOUTSECS is a number, time out after that many seconds."
 (defun proof-done-invisible (span)
   "Callback for ‘proof-shell-invisible-command’.
 Call ‘proof-state-change-hook’."
+  (run-hooks 'proof-state-change-pre-hook)
   (run-hooks 'proof-state-change-hook))
 
 ;;;###autoload