replaced some occurences of (current-buffer) by proof-shell-buffer to

make code more robust

2 files changed, 46 insertions, 40 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index a45b45a2..fa09ede9 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -29,7 +29,7 @@
 ;; This helps see interface between proof-script / proof-shell.
 (eval-when-compile
   (mapcar (lambda (f) 
-	    (autoload f "proof-script"))
+	    (autoload f "proof-shell"))
 	  '(proof-shell-ready-prover
 	    proof-start-queue
 	    proof-shell-live-buffer
@@ -206,19 +206,6 @@ Only call this from a scripting buffer."
   "Return the end of the queue region, or nil if none."
   (and proof-queue-span (span-end proof-queue-span)))
 
-(defun proof-dont-show-annotations ()
-  "Set display values of annotations (characters 128-255) to be invisible."
-  (let ((disp (make-display-table))
-	(i 128))
-	(while (< i 256)
-	  (aset disp i [])
-	  (incf i))
-	(cond ((fboundp 'add-spec-to-specifier)
-	       (add-spec-to-specifier current-display-table disp
-				      (current-buffer)))
-	      ((boundp 'buffer-display-table)
-	       (setq buffer-display-table disp)))))
-
 (defun proof-mark-buffer-atomic (buffer)
   "Mark BUFFER as having been processed in a single step.
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 550d344b..f39479c8 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -36,8 +36,7 @@
 	    proof-set-queue-endpoints
 	    proof-file-to-buffer 
 	    proof-register-possibly-new-processed-file
-	    proof-restart-buffers
-	    proof-dont-show-annotations)))
+	    proof-restart-buffers)))
 
 ;;
 ;; Internal variables used by shell mode
@@ -890,6 +889,23 @@ how far we've got."
   (proof-start-queue nil nil (list (list nil cmd
   'proof-shell-done-invisible))))
 
+(defun proof-shell-dont-show-annotations ()
+  "Set display values of annotations in process buffer to be invisible.
+
+Annotations are characters 128-255."
+  (save-excursion
+    (set-buffer proof-shell-buffer)
+    (let ((disp (make-display-table))
+	  (i 128))
+      (while (< i 256)
+	(aset disp i [])
+	(incf i))
+      (cond ((fboundp 'add-spec-to-specifier)
+	     (add-spec-to-specifier current-display-table disp
+				    proof-shell-buffer))
+	    ((boundp 'buffer-display-table)
+	     (setq buffer-display-table disp))))))
+
 
 
 
@@ -921,7 +937,7 @@ how far we've got."
 
   (add-hook 'comint-output-filter-functions 'proof-shell-filter nil 'local)
   (setq comint-get-old-input (function (lambda () "")))
-  (proof-dont-show-annotations)
+  (proof-shell-dont-show-annotations)
 
   ;; Proof marker is initialised in filter to first prompt found
   (setq proof-marker (make-marker))
@@ -941,29 +957,32 @@ how far we've got."
 		  (cons proof-mode-name (cdr proof-shell-menu)))
 
 (defun proof-shell-config-done ()
-  (accept-process-output (get-buffer-process (current-buffer)))
-
-
-  ;; If the proof process in invoked on a different machine e.g.,
-  ;; for proof-prog-name="rsh fastmachine proofprocess", one needs
-  ;; to adjust the directory:
-  (and proof-shell-cd
-       (proof-shell-insert (format proof-shell-cd
-       ;; under Emacs 19.34 default-directory contains "~" which causes
-       ;; problems with LEGO's internal Cd command
-				   (expand-file-name default-directory))))
-
-  (if proof-shell-init-cmd
-       (proof-shell-insert proof-shell-init-cmd))
-
-  ;; Note that proof-marker actually gets set in proof-shell-filter.
-  ;; This is manifestly a hack, but finding somewhere more convenient
-  ;; to do the setup is tricky.
-
-  (while (null (marker-position proof-marker))
-    (if (accept-process-output (get-buffer-process (current-buffer)) 15)
-	()
-      (error "Failed to initialise proof process"))))
+  "Initialise the specific proover after the child has been configured."
+  (save-excursion
+    (set-buffer proof-shell-buffer)
+    (accept-process-output (get-buffer-process proof-shell-buffer))
+
+    ;; If the proof process in invoked on a different machine e.g.,
+    ;; for proof-prog-name="ssh fastmachine proofprocess", one needs
+    ;; to adjust the directory. Perhaps one might even want to issue
+    ;; this command whenever a new scripting buffer is active?
+    (and proof-shell-cd
+	 (proof-shell-insert (format proof-shell-cd
+				     ;; under Emacs 19.34 default-directory contains "~" which causes
+				     ;; problems with LEGO's internal Cd command
+				     (expand-file-name default-directory))))
+
+    (if proof-shell-init-cmd
+	(proof-shell-insert proof-shell-init-cmd))
+
+    ;; Note that proof-marker actually gets set in proof-shell-filter.
+    ;; This is manifestly a hack, but finding somewhere more convenient
+    ;; to do the setup is tricky.
+
+    (while (null (marker-position proof-marker))
+      (if (accept-process-output (get-buffer-process proof-shell-buffer) 15)
+	  ()
+	(error "Failed to initialise proof process")))))
 
 (eval-and-compile			; to define vars
 (define-derived-mode pbp-mode fundamental-mode