From ef6b56d6a053fa531ccd865b65f389b192bcd8d9 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sat, 22 Feb 2003 17:50:15 +0000
Subject: Updated.

---
 todo | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

(limited to 'todo')

diff --git a/todo b/todo
index 99720d67..d15e738e 100644
--- a/todo
+++ b/todo
@@ -7,20 +7,18 @@ This is an outline file.   Use C-c C-n, C-c C-p or menu to navigate.
 * Proof General Short List of Things to Do for next version
 
 *** Clean up X-symbol support
-     -- configuration for latest version of X-Symbol (Gerwin Klein)
+     -- token configuration for latest version of X-Symbol (Gerwin Klein)
      -- remove on/off setting for all buffers (too slow), use
-        same mechanism as proof-mmm.
+        same mechanism as proof-mmm. [Done; in testing]
 
 *** Finish/cleanup MMM support for Isar.  Document (but who reads it?)
     Add MMM for other provers where relevant
 
-*** Behaviour of X-Symbol and MMM options
-      -- should have "global" behaviour, but apply to future?
-      -- just have local behaviour, add extra option for global?
-      [confusion is that particular buffer may be different from global]
-      -- does it make sense simply to synchronize global with local
-	 whenever local is changed?  
-	  [maybe: turn it off, stays off in new buffers]
+*** Isabelle support: can we somehow add "legacy" support for old 
+      theory files and even allow scripting in ML files?   Maybe
+      not, if this is even beyond what Isar interface would allow
+      (unless we send an ML file line-by-line with ML_command?)
+
  
 * Proof General Infeasibly Long Low-Level List of Things to Do
 
-- 
cgit v1.2.3