diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-12-10 18:08:46 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-12-10 18:08:46 +0000 |
| commit | ea52fc81454ed19269309f1d1f5e122a206b4147 (patch) | |
| tree | e6011133b7f930ca439c03dee9f06d4d2ad4f413 | |
| parent | bb29430d1c69ae8ae19127c8ea338b3070139e9d (diff) | |
Made point stay at top of goals buffer and bottom of response buffer
| -rw-r--r-- | generic/proof-shell.el | 5 | ||||
| -rw-r--r-- | generic/proof.el | 19 |
2 files changed, 18 insertions, 6 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 1da9f236..d86f285f 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -538,9 +538,12 @@ This is a list of tuples of the form (type . string). type is either (proof-shell-maybe-erase-response t t) (set-buffer proof-goals-buffer) + ;; NEW!! 10.12.98 Keep point at beginning of buffer instead + ;; of end. Might be nicer to keep it at "current" subgoal + ;; a la Isamode, but never mind. (erase-buffer) (insert (substring out 0 op)) - (proof-display-and-keep-buffer proof-goals-buffer) + (proof-display-and-keep-buffer proof-goals-buffer (point-min)) (setq ip 0 op 1) diff --git a/generic/proof.el b/generic/proof.el index f50e685a..722f000c 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -161,10 +161,11 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding ;; I get the script buffer made into a dedicated buffer, ;; presumably because the wrong window is selected below? -(defun proof-display-and-keep-buffer (buffer) +(defun proof-display-and-keep-buffer (buffer &optional pos) "Display BUFFER and mark window according to `proof-window-dedicated'. - -Also ensures that point is visible." +If optional POS is present, will set point to POS. +Otherwise move point to the end of the buffer. +Ensure that point is visible in window." (let (window) (save-excursion (set-buffer buffer) @@ -181,8 +182,16 @@ Also ensures that point is visible." ;; da replies: I think it's because of a *missing* ;; save-excursion above around the font-lock stuff. ;; Adding one has maybe fixed this problem. - (goto-char (point-max)) - + ;; 10.12.98 Experiment removing this so that point + ;; doesn't always go to end of goals buffer + ;; RESULT: point doesn't go to end of response + ;; buffer. Hypothesis above was wrong, so this + ;; is re-added and optional POS argument added + ;; for this function. + (goto-char (or pos (point-max))) + (if pos (beginning-of-line)) ; Normalization + + ;; Ensure point visible (or (pos-visible-in-window-p (point) window) (recenter -1))))))) |