Deleted file

1 files changed, 0 insertions, 62 deletions

diff --git a/isa/todo b/isa/todo
deleted file mode 100644
index e4964429..00000000
--- a/isa/todo
+++ /dev/null
@@ -1,62 +0,0 @@
--*- mode:outline -*-
-
-* Things to do for Isabelle
-
-See also ../todo for generic things to do, priority codes.
-
-See also ../isar/todo.  Isar is now main instance for PG, this
-instance less supported.
-
-
-** X Isabelle PG: Non-blocking for .thy loading from .ML files.
-
-** D Isabelle: I think show_sorts -> show_types, how can we reflect this ?
-
-** D Fix mode naming for Isabelle 
-     (might like isa-proofscript-mode -> isa-mode;
-      but this conflicts with entry mechanism for thy/isa mode).
-
-** D Might be nice to unify menus a little more, e.g. add Isabelle for .thy
-
-   But several of the ops there are not relevant for theory files.
-   Well, favourites at least.  What we have at the moment is verging
-   GUI-atrocity: one shouldn't have menus of the same name with
-   different entries, but should rather use greyed out.
-
-** C Improvements to Isabelle that would be nice for Proof General:
-
-   -- ability to remove theorem from theorem database, issued
-   when undoing qed
-
-
-** C X-Symbol support for theory files: bugs at the moment, because
-  of duplicate calls to proof-x-symbol-mode and mess with
-  font-lock initialization.  Problem with current version:
-  visit a.thy, b.thy then turn on xsym.  Broken in b.thy.
-  Seems okay visiting new buffers after that.
-  Must also check interaction with xsym-isa-latex stuff
-  may be broken by removal of mode hook settings.
-  [DvO reports okay].
-  (May need to split extra modes into two parts?)
-
-** B auto-adjust Pretty.setmargin when window is resized.  Use
-  generic code once it's implemented.
-
-** D Implement completion for Isabelle using tables generated by
-  the running process.  Ideally context sensitive.
-  Would be a nice addition. (1 week)
-
-** D Add useful specific commands for Isabelle.  Many could
-  be added.  Would be better to merge in Isamode's menus.
-  (however, probably 2 week's work to bring together Isamode 
-   and proof.el, making some of Isamode generic)
-
-** D Switching to other file with C-c C-o could be more savy
-  with file names and extensions (use some standard function?)
-
-** X Write perl scripts to generate TAGS file for ML and thy files.
-  (60h, any volunteers?) (hard);
-
-** X Manage multiple proofs, perhaps by automatically inserting
-  push_proof() and pop_proof() commands into the proof script.
-  But would lead to unholy mess for script management! (hard!)