-*- mode:outline -*-

* Priorities
============
A (High)   to be fixed before release (Version 2.0)
B (Medium) desirable to fix at some point
C (Low)    probably not worth wasting time on

* This is a list of things which need doing in the generic interface
====================================================================

A Structured review of complete system. Is there redundent code?
  Can some of the LEGO/Coq specific code made generic? Reengineering.
    (2h hhg & tms)

A Update source documentation and manual, in particular document bugs
  and workarounds
  (4h hhg & tms) 

A Implement more generic mechanism for large undos (2h)

    COQ: C-c u inside a Section should reset the whole section, then
         redo defns 

    LEGO: consider Discharge; perhaps unrol to the beginning of the
          module?
    
B Implement proof-find-previous-terminator and bind it to C-c C-a
  (45min tms)

B Technical documentation to record expertise and allow users of other
  proof systems to adopt generic package (40h hhg & tms)

A Fixing up errors caused by pbp-generated commands; currently, script
  management unwisely assumes that pbp commands cannot fail (2h tms)

C pbp code doesn't quite accord with the tech report; in particular it
  decodes annotations eagerly. Lazily would be faster, and it's what
  the tech report claims
  --- djs: probably not much faster, actually.

B file handling could be more robust; perhaps one should always cd to
  the directory corresponding to the script buffer (currently only
  done for the buffer which starts up the proof system) (30min tms)

B replace (current-buffer) by proof-shell-buffer/proof-script-buffer
  where ever possible (30 min tms)

B Allow bib-cite style clicking on Load/Import commands to go to file.

C LEGO and Coq modes overwrite each other.

C We need to go over to piped communication rather than ptys to fix
  the (Solaris) ^G bug. In this circumstance there's a bug in the
  eager annotation code

C Outline-mode does not work due to read-only restrictions of
  protected region

* Here are things to be done to Lego mode
=========================================

A fix Pbp implementation (10h; tms)

A LEGO mode might incorporate changes to Coq mode menu, in particular
  making help refer to the info file (30min tms)

A Sometimes e.g., ~tms/lego/imperative/recursion/Prepare_vc.l,
  annotations are recorded in the object file. This needs to be
  changed in the SML code. (initially 2h tms)

C Mechanism to save object file

A Equiv, Next,... aren't handled properly, because LEGO does not
  refresh the proof state. Perhaps it would be easiest to get LEGO to
  output more information in proof script mode (2h tms)

A Error messages need to be revised e.g., if an import fails, LEGO
  outputs

    Error in file: search: undefined or out of context: should
   (* closing file ./blah.l; time= 0.010000  gc= 0.0  sys= 0.0 *)
   Error: Unwinding to top-level

  but script management only prints the last line. (5h tms)

* Here are things to be done to Coq mode
========================================

B Add Patrick Loiseleur's commands to search for vernac or ml files.

C Sections and files are handled incorrectly.

A Lifted nested lemmas respond incorrectly to C-c u: Coq gets sent the
  correct command if I undo up to the lower lemma, but the buffer
  undoes to the upper lemma.  I.e., if I start Lemma x, then prove
  Lemma y, then finish x, and undo lemma x, then lemma y gets undone
  in the buffer as well. (45min hhg)

B Proof-by-Pointing (10h hhg)

* Emacs19
=========

B Update proof-locked-span so that it detaches the read-only span like 
  what we do in xemacs code (to avoid not being able to type at the
  first character in the buffer if you Undo to that point).
    (1h hhg)

B Commands that use overlapping spans or that delete spans don't work
  (for example: finishing a proof by Save; Undo).
    (5h hhg)