From 1044ec7dbc0335ae122fe062f79219ac310a4f09 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 9 Nov 1998 18:17:08 +0000
Subject: Added proof-script-indent user option, to enable indentation code.
 Disabled by default.  May be activated by particular proof assistants if they
 feel confident about it.  I don't. Made proof-indent be autoloaded as needed.
  Lets pray it won't be.

---
 todo | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'todo')

diff --git a/todo b/todo
index f6664848..2646ce38 100644
--- a/todo
+++ b/todo
@@ -64,13 +64,9 @@ A Revise ProofGeneral.texi and publish LaTeX version as an LFCS
 
 A* Bug in proof-mode configuration of func-menu.  (30mins)
 
-A* FIX INDENTATION CODE, EDITING .ML (& other?) FILES IS CHRONICALLY SLOW.
-  This is going to hit us hard as soon as the mode gets used in
-  earnest.
-  (da, 10mins: disable it!)
-  (da, 2hrs: will investigate if fault lies with Isabelle syntax config)
-  (8hrs, estimated time to fixup indentation code otherwise.  May be
-         best removed altogether, or replaced with elisp code clone)
+C Improve indentation code and see why it's so slow (at
+  least for Isabelle).   Enable it for particular provers if
+  it works okay  (but must test in on large files).
 
 C Regions in script buffer have nice "name" property and configurers
   have to set regexps carefully so that it works, but is it actually
-- 
cgit v1.2.3