diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 18 | ||||
| -rw-r--r-- | generic/proof-script.el | 7 | ||||
| -rw-r--r-- | generic/proof-shell.el | 16 |
3 files changed, 38 insertions, 3 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-script.el b/generic/proof-script.el index e67a7774..7d9afe22 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2565,9 +2565,10 @@ finish setup which depends on specific proof assistant configuration." ;; Additional key def for (first character of) terminal string (if proof-terminal-string (progn - (define-key proof-mode-map - (vconcat [(control c)] (vector (aref proof-terminal-string 0))) - 'proof-electric-terminator-toggle) +;; This key-binding was disabled following a request in PG issue #160. +;; (define-key proof-mode-map +;; (vconcat [(control c)] (vector (aref proof-terminal-string 0))) +;; 'proof-electric-terminator-toggle) (define-key proof-mode-map (vector (aref proof-terminal-string 0)) 'proof-electric-terminator))) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 13da8d98..51305eef 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1110,6 +1110,22 @@ 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))) + ;; 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))) + ;; 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 |