diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-08-20 16:53:46 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-08-20 16:53:46 +0000 |
| commit | 6f59f23139118fbec70c409d94b79cec36845db9 (patch) | |
| tree | 1d02ab46da24ac45a061f82abaa30745ebd54fff | |
| parent | 8fb1f3775018e7ce66e2ba241cd467f9339a4fda (diff) | |
proof-goto-end-of-locked-if-pos-not-visible-in-window:
Check that there is active scripting buffer, in Isabelle there might not be.
| -rw-r--r-- | generic/proof-script.el | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index e5254788..e40696dc 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -588,14 +588,15 @@ Must be an active scripting buffer." (defun proof-goto-end-of-locked-if-pos-not-visible-in-window () "If the end of the locked region is not visible, jump to the end of it. A possible hook function for proof-shell-handle-error-hook. -Must be an active script buffer." +Does nothing if there is no active scripting buffer." (interactive) - (let* ((pos (save-excursion - (set-buffer proof-script-buffer) - (proof-locked-end)))) - (or (pos-visible-in-window-p pos (get-buffer-window - proof-script-buffer t)) - (proof-goto-end-of-locked-interactive)))) + (if proof-script-buffer + (let* ((pos (save-excursion + (set-buffer proof-script-buffer) + (proof-locked-end)))) + (or (pos-visible-in-window-p pos (get-buffer-window + proof-script-buffer t)) + (proof-goto-end-of-locked-interactive))))) ;; da: NEW function added 28.10.98. ;; This is used by toolbar follow mode (which used to use the function |