Bufhist erase when buffer writable.

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