aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-goals.el
diff options
context:
space:
mode:
Diffstat (limited to 'generic/pg-goals.el')
-rw-r--r--generic/pg-goals.el9
1 files changed, 3 insertions, 6 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 35ea669c..e3e53c5a 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -101,13 +101,10 @@ Converts term substructure markup into mouse-highlighted extents."
;; Only display if string is non-empty.
(unless (string-equal string "")
+ (setq buffer-read-only nil)
(insert string)
-
- ;; Record a cleaned up version of output string
- (setq proof-shell-last-output
- (buffer-substring (point-min) (point-max)))
-
- (set-buffer-modified-p nil) ; nicety
+ (setq buffer-read-only t)
+ (set-buffer-modified-p nil)
;; Keep point at the start of the buffer.
(proof-display-and-keep-buffer