diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-14 13:44:14 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-14 13:44:14 +0000 |
| commit | 6f92823397844051832a9e82c6e38005f2a2c62e (patch) | |
| tree | 55792708b233d39758af42f1566d114687450b20 /lego | |
| parent | 61df75856fa282284a4805c9df2d0f81806c225d (diff) | |
fixed bug in lego-shell-adjust-line-width (It now monitors the
proof-goals-buffer)
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/lego.el | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/lego/lego.el b/lego/lego.el index a0292bdb..7ccba295 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -323,18 +323,21 @@ Given is the first SPAN which needs to be undone." ;; running and is out of sync with the screen width (defun lego-shell-adjust-line-width () - "Use LEGO's pretty printing facilities to adjust output line width." - (save-excursion - (set-buffer proof-shell-buffer) - (and (proof-shell-live-buffer) + "Use LEGO's pretty printing facilities to adjust output line width. +Checks the width in the `proof-goals-buffer'" + (and (buffer-live-p proof-goals-buffer) + (proof-shell-live-buffer) + (save-excursion + (set-buffer proof-goals-buffer) (let ((current-width - ;; FIXME da: I suspect this is the wrong window to - ;; check the width of. Probably we want the width - ;; of proof-goals-buffer? - (window-width (get-buffer-window proof-shell-buffer)))) + ;; Actually, one might sometimes + ;; want to get the width of the proof-response-buffer + ;; instead. Never mind. + (window-width (get-buffer-window proof-goals-buffer)))) (if (equal current-width lego-shell-current-line-width) () ; else (setq lego-shell-current-line-width current-width) + (set-buffer proof-shell-buffer) (insert (format lego-pretty-set-width (- current-width 1))) ))))) |