Quick fix for multiple file problem when current scripting buffer is retracted by prover.

3 files changed, 31 insertions, 11 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 624a468e..2b6de678 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -859,8 +859,9 @@ deletes the region corresponding to the proof sequence."
   (let ((start (span-start span))
         (end (span-end span))
 	(kill (span-property span 'delete-me)))
-    (proof-set-locked-end start)
-    (proof-set-queue-end start)
+    (unless (proof-locked-region-empty-p)
+      (proof-set-locked-end start)
+      (proof-set-queue-end start))
     (delete-spans start end 'type)
     (delete-span span)
     (if kill (delete-region start end))))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 28c60ddc..b2e6dd30 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -786,11 +786,25 @@ arrive."
 	 (let ((current-included proof-included-files-list))
 	   (setq proof-included-files-list
 		 (funcall proof-shell-compute-new-files-list message))
-	   (proof-restart-buffers
-	    (remove (car-safe proof-script-buffer-list)
-		    (proof-files-to-buffers
-		     (set-difference current-included
-				     proof-included-files-list))))))
+	   (let
+	       ((scrbuf (car-safe proof-script-buffer-list)))
+	       (proof-restart-buffers
+		;; FIXME: multiple files needs fixing here!!
+		;; (remove (car-safe proof-script-buffer-list)
+		(proof-files-to-buffers
+		 (set-difference current-included
+				 proof-included-files-list)))
+					; )
+	       (cond
+		((not scrbuf))
+		((eq scrbuf (car-safe proof-script-buffer-list)))
+		(t	
+		 (setq proof-script-buffer-list 
+		       (cons scrbuf proof-script-buffer-list))
+		 (save-excursion
+		   (set-buffer scrbuf)
+		   (proof-init-segmentation)))))
+	   ))
 	(t
 	 (proof-shell-message message)
 	 (proof-response-buffer-display message
diff --git a/generic/proof.el b/generic/proof.el
index 29e89e2d..ed78f397 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -26,17 +26,25 @@
 
 (require 'proof-splash)			; splash screen
 
+;;;
+;;; Emacs libraries
+;;;
+
 ;; cl is dumped with my XEmacs 20.4, but not FSF Emacs 20.2.
 (require 'cl)				
 
-
 ;; browse-url function doesn't seem to be autoloaded in
 ;; XEmacs 20.4, but it is in FSF Emacs 20.2.
 (or (fboundp 'browse-url)
     (autoload 'browse-url "browse-url"
       "Ask a WWW browser to load URL." t))
 
+(autoload 'font-lock-fontify-region "font-lock")
+(autoload 'font-lock-append-text-property "font-lock")
+
+;;;
 ;;; Autoloads for main code
+;;;
 
 (autoload 'proof-mode "proof-script"
   "Proof General major mode class for proof scripts.")
@@ -55,8 +63,6 @@
 (autoload 'proof-shell-available-p "proof-shell"
   "Returns non-nil if there is a proof shell active and available.")
 
-(autoload 'font-lock-fontify-region "font-lock")
-(autoload 'font-lock-append-text-property "font-lock")
 ;;;
 ;;; Global variables
 ;;;
@@ -103,7 +109,6 @@ The cdr of the list of corresponding file names is a subset of
 
 
 
-
 ;;;
 ;;; Utilities/macros used in several files  (proof-utils)
 ;;;