diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-09-21 15:36:39 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-09-21 15:36:39 +0000 |
| commit | 9d1bf8b956e4a2f9e7aa56680104f25c5c474f01 (patch) | |
| tree | 2d08b4f7390adfe804aef6aa3919ad81c73504cc /generic/proof-shell.el | |
| parent | 771fb3ec1d8666286522e397dd6aabdf053c6cb2 (diff) | |
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.
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 14 |
1 files 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 |