From fe91bb443c5c0bf7c2d9800d599cff6e45d2197b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 6 Sep 2009 13:57:41 +0000
Subject: Bufhist erase when buffer writable.

---
 generic/pg-goals.el | 18 ++++++++++--------
 1 file 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
-- 
cgit v1.2.3