aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-06-27 15:27:29 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-06-27 15:27:29 +0000
commit840f589d751c08906ab6275c73c241167bb66214 (patch)
tree54cc67c932043303b4d1ca5d67d1b3a152acabdc /isar
parentef2a6fe289ff21a2d215fbc30637b9e1bd34f474 (diff)
Note about typing in shell buffer
Diffstat (limited to 'isar')
-rw-r--r--isar/todo7
1 files changed, 5 insertions, 2 deletions
diff --git a/isar/todo b/isar/todo
index 22507b4f..f0be8852 100644
--- a/isar/todo
+++ b/isar/todo
@@ -14,7 +14,10 @@ Isabelle's pretty-printing subsystem);
** C tune behaviour of goals/response buffers (e.g. hide empty
response buffers when using 2 buffer model);
-** C eliminate x-symbol-isar.el in favour of shared x-symbol-isabelle.el;
-
** D Combine with isa/ to get single Isabelle PG instance, somehow?
Then users could use both proof languages in the same session.
+
+** D Fixup so that typing in shell buffer updates locked buffer status.
+It works in Isabelle/classic, why not here? (But users shouldn't
+type in shell buffer, anyway).
+