done: exit isar;

added comment about output performance;

1 files 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.