From 48bcb3395e21feb0669843521eb6b0ffe1e9f8d7 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Thu, 21 Sep 2000 13:17:48 +0000
Subject: done: exit isar; added comment about output performance;

---
 todo | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/todo b/todo
index 0a6ce1f7..3b823675 100644
--- a/todo
+++ b/todo
@@ -34,8 +34,6 @@ C The PG isabelle-completion-table seems to be subject to case-fold, which
 
 B Keybindings for processing theory in thy mode gone??
 
-B Exiting isar broken?
-
 C Undoing comments with FSF Emacs weirdness.
  Noticed with Emacs 20.6.1.  Seems to affect all provers.
  Workaround:  use C-c C-RET or C-c C-r instead.
@@ -118,6 +116,9 @@ X Solaris bugs: font locking and button enabling.
   Patch already added to pre-release.
   Does it need adjusting to turn on output in case of error/interrupt?
 
+  mmw: Performance problems in isa and isar have been fixed by
+  removing eager annotations almost everywhere.
+
 **** C Add improvements to script movement in electric terminator mode.
   Some commented regions in code.  E.g. automatic newline/space after
   C-c C-BS.
-- 
cgit v1.2.3