-*- mode:outline -*-

* Things to do for Isabelle

See also ../todo for generic things to do, priority codes.

** 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!)