updated;

1 files changed, 3 insertions, 16 deletions

diff --git a/isar/todo b/isar/todo
index 37f1d500..944083dc 100644
--- a/isar/todo
+++ b/isar/todo
@@ -4,17 +4,8 @@
 
 See also ../todo for generic things to do, priority codes.
 
-** B switch to ProofGeneral.undo (after Isabelle99-1 is out!);
-
-** C fix '{{' and '}}' keywords (e.g. proper font-lock, indentation);
-unfortunately the present word boundary regexp does not work since { }
-are already part of comment syntax;
-
 ** C undo 'use' command: unlock corresponding ML file;
 
-** C interactive support for diagnostic commands: easy way to run
-thm/prop/term/typ on region in an ad-hoc fashion;
-
 ** C provide template for empty theory (or even just for Scratch.thy);
 
 ** C proper proof-by-pointing support (hard; needs major reworking of
@@ -24,14 +15,10 @@ Isabelle's pretty-printing subsystem);
 nice if current indentation stack would be somehow stored within the
 extend(s) processed last;
 
-** C eliminate explicit ";" terminator; rather refer to regexp (note:
-requires {{ }} to be fixed; ideally, current set of keywords would be
-retrieved from the running process, in order to gain robustness);
-
 ** C tune behaviour of goals/response buffers (e.g. hide empty
 response buffers when using 2 buffer model);
 
-** D Combine with isa/ to get single Isabelle PG instance, somehow?
-
-Then users could use both proof languages.
+** 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.