aboutsummaryrefslogtreecommitdiffhomepage
path: root/lego/lego.el
diff options
context:
space:
mode:
Diffstat (limited to 'lego/lego.el')
-rw-r--r--lego/lego.el6
1 files changed, 2 insertions, 4 deletions
diff --git a/lego/lego.el b/lego/lego.el
index 2234bb12..46b2cb5c 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -272,10 +272,8 @@ Given is the first SPAN which needs to be undone."
(defun lego-shell-adjust-line-width ()
"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)
+ (and (proof-shell-live-buffer)
+ (proof-with-current-buffer-if-exists proof-goals-buffer
(let ((current-width
;; Actually, one might sometimes
;; want to get the width of the proof-response-buffer