From 9d1bf8b956e4a2f9e7aa56680104f25c5c474f01 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 21 Sep 1999 15:36:39 +0000
Subject: proof-shell-grab-lock runs proof-state-change-hook. This results in
 some flickering of the toolbar (buttons disabled while region is pink), but
 is The Right Thing.

Removed "Inferior" from buffer names.
---
 generic/proof-shell.el | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 3adfbdf7..e1c9736c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -158,11 +158,12 @@ No error messages.  Useful as menu or toolbar enabler."
   (and (proof-shell-live-buffer)
        (not proof-shell-busy)))
 
-;; FIXME: note: removed optional 'relaxed' arg
 (defun proof-grab-lock ()
-  "Grab the proof shell lock."
+  "Grab the proof shell lock, starting the proof assistant if need be.
+Runs proof-state-change-hook to notify state change."
   (proof-shell-ready-prover)
-  (setq proof-shell-busy t))
+  (setq proof-shell-busy t)
+  (run-hooks 'proof-state-change-hook))
 
 (defun proof-release-lock ()
   "Release the proof shell lock."
@@ -209,8 +210,11 @@ Does nothing if proof assistant is already running."
 	  (setq proof-prog-name (read-shell-command "Run process: "
 						    proof-prog-name))))
     (let ((proc
-	   ;; "Inferior" is Emacs terminology for sub-shell processes.
-	   (concat "Inferior "
+	   
+	   (concat 
+	    ;; "Inferior" is Emacs terminology for sub-shell processes.
+	    ;; "Inferior " used to be part of the name, now removed 
+	    ;; for brevity.
 		   ;; Try to pick useful part of command name
 		   ;;  -- basename component of command less arguments
 		   (substring proof-prog-name
-- 
cgit v1.2.3