diff options
| -rw-r--r-- | coq/coq.el | 6 | ||||
| -rw-r--r-- | generic/proof-config.el | 13 |
2 files changed, 19 insertions, 0 deletions
@@ -614,6 +614,11 @@ and read by function `coq-empty-action-list-command'.") ;;TODO update docstring and comment +(defun coq-open-goals-p () + "Return non nil if we are inside a proof, see `proof-shell-open-goals-p'." + (car (cdr (cdr (coq-last-prompt-info-safe))))) + + (defun coq-set-state-infos () "Set the last locked span's state number to the number found last time. This number is in the *last but one* prompt (variable `coq-last-but-one-statenum'). @@ -1897,6 +1902,7 @@ at `proof-assistant-settings-cmds' evaluation time.") coq-compile-auto-save coq-lock-ancestors coq-diffs)) (setq proof-goal-command-p #'coq-goal-command-p + proof-shell-last-cmd-left-goals-p #'coq-open-goals-p proof-find-and-forget-fn #'coq-find-and-forget pg-topterm-goalhyplit-fn #'coq-goal-hyp proof-state-preserving-p #'coq-state-preserving-p) 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 |