From 587543b1038b52b1adc2bce47f52d47d146d6121 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 6 Oct 1999 10:54:06 +0000
Subject: Updated

---
 CHANGES | 3 +++
 todo    | 3 ++-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index e29e3adf..bc7754ca 100644
--- a/CHANGES
+++ b/CHANGES
@@ -48,6 +48,9 @@ Generic Changes
   scripting on or off in current buffer.  This is a handy way to
   discard or finish off scripting in an unfinished buffer
   triggering the deactivation mechanism mentioned above.
+  Switching on scripting in a buffer may cause the proof
+  assistant to load files it depends on, so it is also handy
+  to see what happens before scripting begins in the buffer.
 
 * Cleaned up example files so all demonstrate same theorem "conj_comms".
   Would be nice to add more theorems to compare scripts/proofs in
diff --git a/todo b/todo
index 0d7720ac..1190081b 100644
--- a/todo
+++ b/todo
@@ -48,7 +48,8 @@ A Pending work, in progress [da]:
     - investigate bug fix for vacuous locked regions
     - document proof-mouse-track-insert (new name for proof-send-span, re-enabled), proof-toggle-scripting, new configuration options.
 
-B Fix colouring of response buffer, may be broken.
+B Fix colouring of response buffer, may be broken.  The idea was
+  that the latest message would always be highlighted, I think.
 
 B Usability enhancement: remove stupid "I don't know what I should be doing"
   errors and replace with something more informative.
-- 
cgit v1.2.3