aboutsummaryrefslogtreecommitdiffhomepage
path: root/todo
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2000-06-08 19:44:12 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2000-06-08 19:44:12 +0000
commit16ec26fb7f102aa37c9546d95f0f61109699a6be (patch)
treee1b5324289080961a66c56f98c00b6ab13d35173 /todo
parentfcb6f0745c966fe600fc5b54ef8a21ca2944c228 (diff)
Improved indentation code; enabled by default;
Diffstat (limited to 'todo')
-rw-r--r--todo4
1 files changed, 0 insertions, 4 deletions
diff --git a/todo b/todo
index c9fda72d..e802b380 100644
--- a/todo
+++ b/todo
@@ -538,10 +538,6 @@ C New modules:
function to be invoked instead? (Cf font lock).
Or via a new generic mechanism for matching or invoking a fn.
-*** D 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).
-
*** D ROBUSTness: deal gracefully with possibility that goals buffer is
killed during session. (2h)