Fixing #154.

2 files changed, 36 insertions, 0 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 8ce53168..8bb40634 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1187,6 +1187,24 @@ If nil, use the whole of the output from the match on
   :type '(choice (const nil) regexp)
   :group 'proof-shell)
 
+(defcustom proof-shell-empty-action-list-command nil
+  "A function returning a list of commands (strings) to be sent
+to the prover when the last command in the queue has been
+performed. Typically to ask for some informational
+display (goals, etc).
+
+The function takes as argument the last command in the queue.
+
+NOTE 1: The commands will be tagged invisible, i.e. not related
+to a place in the buffer.
+
+NOTE 2: The commands should NOT have any effect on the state of
+the prover. Otherwise running the script outside pg would be
+inconsistent."
+  :type 'function
+  :group 'proof-shell)
+
+
 (defcustom proof-shell-eager-annotation-start nil
   "Eager annotation field start.  A regular expression or nil.
 An \"eager annotation indicates\" to Proof General that some following output
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 13da8d98..2c9f9727 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1110,6 +1110,24 @@ contains only invisible elements for Prooftree synchronization."
 	(setq cbitems (cons item
 			    (proof-shell-slurp-comments)))
 
+        ;; If proof-action-list is empty after removing the already
+        ;; processed actions and the last action was not already
+        ;; added by proof-shell-empty-action-list-command (prover
+        ;; specific), call it.
+        (when (and (null proof-action-list)
+                   (not (memq 'empty-action-list flags)))
+          (let* ((cmd (mapconcat 'identity (nth 1 item) " "))
+                (extra-cmds (apply proof-shell-empty-action-list-command (list cmd)))
+                (dummy (message "extra-cmds = %S" extra-cmds))
+                ;; 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))
+                 (dummy (message "extra-items = %S" extra-items)))
+            ;; action-list should be empty at this point
+            (setq proof-action-list (append extra-items proof-action-list))))
+
 	;; This is the point where old items have been removed from
 	;; proof-action-list and where the next item has not yet been
 	;; sent to the proof assistant. This is therefore one of the