diff options
| author | David Aspinall | 1999-10-06 10:54:06 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-10-06 10:54:06 +0000 |
| commit | 587543b1038b52b1adc2bce47f52d47d146d6121 (patch) | |
| tree | 0052d287ce500aef554f482203b1da46d328ae5d | |
| parent | 41c4dc9b22c28832fd8d0a7b99e2412bc8eff2ff (diff) | |
Updated
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | todo | 3 |
2 files changed, 5 insertions, 1 deletions
@@ -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 @@ -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. |
