diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2011-11-15 13:50:51 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2011-11-15 13:50:51 +0000 |
commit | 17e3598c76cb426e96b973fb49c53a4227877383 (patch) | |
tree | 6ebb3da0beb65bd913478b2bd036435e58dbca57 /generic/proof-shell.el | |
parent | 0d6be0aee27af7773714e2baa7ce344c11b41f53 (diff) |
Quick stab at support for switching to proof shell when interactive support expected, see Trac #430
Diffstat (limited to 'generic/proof-shell.el')
-rw-r--r-- | generic/proof-shell.el | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 4015f3a8..e2146249 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1086,8 +1086,9 @@ and indentation. Assumes `proof-script-buffer' is active." (defun proof-shell-process-urgent-message (start end) "Analyse urgent message between START and END for various cases. -Cases are: included file, retracted file, cleared response buffer, -variable setting, PGIP response, or theorem dependency list. +Cases are: *trace* output, included/retracted files, cleared +goals/response buffer, variable setting, xml-encoded PGIP response, +theorem dependency message or interactive output indicator. If none of these apply, display the text between START and END. @@ -1124,6 +1125,12 @@ ends with text matching `proof-shell-eager-annotation-end'." ((proof-looking-at-safe proof-shell-theorem-dependency-list-regexp) (proof-shell-process-urgent-message-thmdeps)) + ((proof-looking-at-safe proof-shell-theorem-dependency-list-regexp) + (proof-shell-process-urgent-message-thmdeps)) + + ((proof-looking-at-safe proof-shell-interactive-prompt-regexp) + (proof-shell-process-interactive-prompt-regexp)) + (t (proof-shell-process-urgent-message-default start end)))) @@ -1211,6 +1218,14 @@ inverse to `proof-register-possibly-new-processed-file'." (cons (split-string names sep) (split-string deps sep))))) +(defun proof-shell-process-interactive-prompt-regexp () + "Action taken when `proof-shell-interactive-prompt-regexp' is observed." + (when (and (proof-shell-live-buffer) + ; not already visible + t) + (switch-to-buffer proof-shell-buffer) + (message "Prover expects input in %s buffer" proof-shell-buffer))) + ;; ;; urgent message utilities ;; |