aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall1999-10-06 10:54:06 +0000
committerDavid Aspinall1999-10-06 10:54:06 +0000
commit587543b1038b52b1adc2bce47f52d47d146d6121 (patch)
tree0052d287ce500aef554f482203b1da46d328ae5d
parent41c4dc9b22c28832fd8d0a7b99e2412bc8eff2ff (diff)
Updated
-rw-r--r--CHANGES3
-rw-r--r--todo3
2 files changed, 5 insertions, 1 deletions
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.