-*- 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 Write function proof-retract-file. (hhg? 30min)

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?

A Multiple files are sometimes handled incorrectly, because the
  function `proof-steal-process' cannot figure out that some files have
  already been processed. This is most likely caused by the ad-hoc
  equality test on file names. Instead, one could employ
  the built-in `file-truename' to trigger *canonical* file names.
  (1h tms)

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)

B Support for x-symbols package 

C XEmacs sessions seem to grow excessively in terms of memory
  allocation. Perhaps some of the spans aren't removed properly?
  Setting a limit on the size of the process buffer doesn't seem to
  help. 

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

B Remove LEGO-specific code in proof.el: for example,
  proof-shell-eager-annotation-end, proof-included-files-list.
  (added by hhg)

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

A set up regular definitions to support definitions of the form
  id == term (10min; tms)

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 set proof-commands-regexp to support indentation for commands
						    (10min hhg)

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)
  [ This seems to have corrected itself... hhg ]

B Proof-by-Pointing (10h hhg)

A Add coq-add-tactic with a tactic name, which adds that tactic to the 
  undoable tactics and to the font-lock. (2h hhg)

* Emacs19
=========

B The proof-locked-span isn't set to read-only, because overlays don't 
  have that capability.  This needs to be done with text-regions.
  (2hr hhg)

B Replace running-(xemacs|emacs19) in proof.el by fboundp. (20min tms)

A Replace recursion with while-loop in span-overlay. (2h hhg)