diff options
| -rw-r--r-- | generic/pg-goals.el | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el index a0b125a4..f98859ba 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -96,19 +96,21 @@ Converts term substructure markup into mouse-highlighted extents." ;; Erase the goals buffer and add in the new string (set-buffer proof-goals-buffer) + (setq buffer-read-only nil) + (unless (eq 0 (buffer-size)) (bufhist-checkpoint-and-erase)) ;; Only display if string is non-empty. (unless (string-equal string "") - (setq buffer-read-only nil) - (insert string) - (setq buffer-read-only t) - (set-buffer-modified-p nil) - - ;; Keep point at the start of the buffer. - (proof-display-and-keep-buffer - proof-goals-buffer (point-min))))) + (insert string)) + + (setq buffer-read-only t) + (set-buffer-modified-p nil) + + ;; Keep point at the start of the buffer. + (proof-display-and-keep-buffer + proof-goals-buffer (point-min)))) ;; ;; Actions in the goals buffer |