From 9ab3b791475bf2a11c3a19ede4449c87902dd95f Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Tue, 10 Feb 1998 14:46:45 +0000
Subject: *** empty log message ***

---
 todo | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/todo b/todo
index f4af3662..9545d6ea 100644
--- a/todo
+++ b/todo
@@ -19,7 +19,9 @@ o It would be nice to have a version ported to emacs19 (or
   doubtless differences in font-locking and menu code which will
   require some work.
 
-o file handling could be more robust
+o file handling could be more robust; perhaps one should always cd to
+  the directory corresponding to the script buffer (currently only
+  done for the buffer which starts up the proof system)
 
 o LEGO and Coq modes overwrite each other.
 
@@ -27,6 +29,9 @@ o We need to go over to piped communication rather than ptys to fix
   the (Solaris) ^G bug. In this circumstance there's a bug in the
   eager annotation code
 
+o Outline-mode does not work due to read-only restrictions of
+  protected region
+
 * Here are things to be done to Lego mode
 =========================================
 
@@ -36,6 +41,19 @@ o undo support for LEGO needs to consider Discharge; perhaps unrol to
 o LEGO mode might incorporate changes to Coq mode menu, in particular
   making help refer to the info file.
 
+o Sometimes e.g., ~tms/lego/imperative/recursion/Prepare_vc.l,
+  annotations are recorded in the object file. This needs to be
+  changed in the SML code.
+
+o Mechanism to save object file (does this apply to Coq as well?)
+
+o Equiv, Next,... aren't handled properly, because LEGO does not
+  refresh the proof state. Perhaps it would be easiest to get LEGO to
+  output more information in proof script mode
+
+o due to bugs in the LEGO system, object files may fail.
+  Script-management needs to be aware of this problem.
+
 * Here are things to be done to Coq mode
 ========================================
 
-- 
cgit v1.2.3