From 5807535598911346f09db0091ccbb2d1c3283433 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 27 May 2020 19:03:36 +0200
Subject: Add proof-shell-last-cmd-left-goals-p.

Prover specific analyzis of the last prompt/output to determine if
there are open goals left.
---
 generic/proof-config.el | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'generic')

diff --git a/generic/proof-config.el b/generic/proof-config.el
index c10c0ee0..14fcdcac 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1499,6 +1499,19 @@ on `proof-shell-eager-annotation-start' and
   :type '(choice (const nil) regexp)
   :group 'proof-shell)
 
+(defcustom proof-shell-last-cmd-left-goals-p nil
+  "A function to test: are we currently inside a proof?
+
+This function takes no argument and should use
+`proof-shell-last-prompt' and `proof-shell-last-output' to
+determine whether the last command ended up inside a
+proof (either by remaining inside one or opening a new one), or
+outside of any proof.
+"
+  :type 'function
+  :group 'proof-script)
+
+
 
 ;;
 ;; 3c. tokens mode: turning on/off tokens output
-- 
cgit v1.2.3