diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2001-07-23 09:16:01 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2001-07-23 09:16:01 +0000 |
| commit | 7f649a353ae3be418d95ddf18791a054852f25d0 (patch) | |
| tree | 5c2ec218215f99b39f41eef18e0ddecd05875309 | |
| parent | b538a5e24c714b9bb9329567dcfa37ec81b08a55 (diff) | |
Bug report from Robert Schneck. Make proof-shell-restart start shell. Goals display convention, not hack.
| -rw-r--r-- | generic/proof-shell.el | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 32080340..afe3d938 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -423,13 +423,17 @@ object files, used by Lego and Coq)." (progn (proof-interrupt-process) (proof-shell-wait))) - ;; Now clear all context - (proof-script-remove-all-spans-and-deactivate) - (proof-shell-clear-state) - (if (and (buffer-live-p proof-shell-buffer) - proof-shell-restart-cmd) - (proof-shell-invisible-command - proof-shell-restart-cmd))) + (if (not (proof-shell-live-buffer)) + ;; If shell not running, start one now. + ;; (Behaviour suggested by Robert Schneck) + (proof-shell-start) + ;; Otherwise, clear all context for running prover + (proof-script-remove-all-spans-and-deactivate) + (proof-shell-clear-state) + (if (and (buffer-live-p proof-shell-buffer) + proof-shell-restart-cmd) + (proof-shell-invisible-command + proof-shell-restart-cmd)))) @@ -938,7 +942,7 @@ which see." ;; Find the last goal string in the output (while (string-match proof-shell-start-goals-regexp string start) (setq start (match-end 0))) - ;; Ugly hack: provers with special characters don't include + ;; Convention: provers with special characters don't include ;; the match in their goals output. Others do. (unless proof-shell-first-special-char (setq start (match-beginning 0))) |