From 7f649a353ae3be418d95ddf18791a054852f25d0 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 23 Jul 2001 09:16:01 +0000
Subject: Bug report from Robert Schneck.  Make proof-shell-restart start
 shell.  Goals display convention, not hack.

---
 generic/proof-shell.el | 20 ++++++++++++--------
 1 file 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)))
-- 
cgit v1.2.3