diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-26 14:40:57 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-26 14:40:57 +0000 |
| commit | 46f1aac56ac61e8b76e4ce6a57ff36806582a8b4 (patch) | |
| tree | 0d0a5625bf3fd2bd06097e8e4a391740d24df8ea /generic | |
| parent | 8b698fd0e35fd0d1b9e297445d0906eddd279ef5 (diff) | |
Allow proof-goto-end-of-locked to work again if no active scripting buffer.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index efe17747..86e44346 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -447,8 +447,11 @@ If non-nil, point is left where it was." If interactive or SWITCH is non-nil, switch to script buffer first." (interactive) (proof-with-script-buffer - (if (and (not (get-buffer-window proof-script-buffer)) + (if ;; there is an active scripting buffer and it's not displayed + (and proof-script-buffer + (not (get-buffer-window proof-script-buffer)) (or switch (interactive-p))) + ;; display it (switch-to-buffer proof-script-buffer) (goto-char (proof-unprocessed-begin))))) |