path: root/todo

-*- mode:outline -*-
$Id$

This is an outline file.   Use C-c C-n, C-c C-p or menu to navigate.

=================================================================

* THINGS TO DO BEFORE 3.5 RELEASE

*** Emacs Bug Roundup
    --- xemacs support for nested comments
    --- xemacs undo in read-only regions 

*** Clean up X-symbol support
     -- token configuration for latest version of X-Symbol (Gerwin Klein, done?)
     -- remove on/off setting for all buffers (too slow), use
        same mechanism as proof-mmm. [Done; in testing]
     -- Check x-symbol support in provers other than Isabelle

*** Finish/cleanup MMM support for Isar.  Document (but who reads it?)
       Add MMM for other provers where relevant

*** Isabelle support: can we somehow add "legacy" support for old 
      theory files and even allow scripting in ML files?   Maybe
      not, if this is even beyond what Isar interface would allow
      (unless we send an ML file line-by-line with ML_command?)

*** Isabelle tweaks
     -- theorem dependencies on spoils ordinary response buffer output
     (dependency info *after* response display loses)

*** Check multiple file support in Isabelle -- maybe has become buggy


 
* Proof General Infeasibly Long Low-Level List of Things to Do


** 0. Contents

 1. Priorities
 2. Things to do in the generic interface
 3. Things to do for the documentation
 4. Emacs issues
 5. Things to do for Proof-by-Pointing
 6. Things to do for Web Pages, Distribution
 7. Future improvements to take advantage of newer Emacsen
 8. Bugs in other software beyond our control
 9. Stable version release checklist
10. Things to do for Proof General Project
 
    See <prover>/todo for things to do for each prover.

** 1. Priorities

A (High)	e.g. to be fixed ASAP for next pre-release 
B		e.g. to be fixed before next release
C (Medium)	e.g. would be nice to fix before next release; not crucial
D		e.g. desirable to fix at some point
X (Low)		e.g. probably not worth spending time on


** 2. Things to do in the generic interface

*** PGIP SUPPORT (minimal for Isabelle patch):
      -- settings with categories

*** [ Don't query save before retraction ?? ]

*** C Implement optional arg to next/undo which doesn't update
      display (so user can retain something else on screen)

*** A fix display anomaly for Isar output with shrink windows:
    display splits window unexpectedly.

*** B Cleanup display during settings processing.

*** B Generic adjusting of pretty-printer line width (currently
    implemented in several instances)

*** B document and simplify proof-script-span-context-menu-extensions

*** B Documentation:
      Check new doc for hiding; add doc for dependencies, tracing.
      Moving spans; navigating through locked region.  
      Favourite menu.

*** B generalize from Isabelle's "atomic scripting" theory file mode
      to allow other instances which do not allow incremental
      processing of files in major or auxiliary file types.
      E.g. twelf, ACL2, LambdaCLAM.
      Also, add the atomic scripting handling for Isabelle/Isar.

*** B Move over to new better designed parsing function mechanism.

*** B Generalize electric terminator mode for other parsing mechanisms.

*** B Add parameter for help function so HOL help works nicely

*** C Add output highlighting to minibuffer in proof-shell-message.
    (Quite tricky to get text properties onto text in minibuffer...)

*** C Extensions with semantic tokens
      Look at the Semantic Navigator package.  Implements persistent
      database of tokens.

*** C Fix byte compilation
      Problem with proof-ass macro mechanism -- gets expanded during compilation.

*** D Isabelle PG: Non-blocking for .thy loading from .ML files.

*** D Bugs with extents: 
      Sometimes probs if try to assert a whole file while one is
      being processed:     (proof-set-queue-start end) call in
      proof-done-advancing finds that queue span is detached.
      Code is now robust for this.  But why detach anyway?

*** D ChangeLog generation still not right.  
      Probs: duplicated entries when runs several times in same day.
      Suggested fix: use rcs2log to generate the entire log, just take
      a sensible number of lines from it.
      (Ideal would be to get until a given date)

*** B proof-shell-restart should clear response buffer (only noticed with
  proof-tidy-response=nil)

*** B TESTING. 
    - Add automatic testing mechanism to test user-level functions PG
    - Test schedule for things to try with a new instantiation

*** B Add a new configuration setting for matching proof commands
  which have no undo effect --- should be treated like comments
  for undo.  Perhaps would be useful for Isabelle, HOL, at least,
  although it's tricky to see how it would be completely *safe*.
  [ See discussion with Pierre re Coq undo command categories ]

*** C Fix the doc makefiles to adapt the image flag in PG-adapting.tex
      properly, for dvi/ps targets

*** C Clean up assert-until-point stuff: should have just one
  function, as a subroutine of assert-next-command; and no bizarre
  never-used arguments!

*** C make pretty printer line width altering generic.
  Make a generic hook (or hook-constructing macro) to adjust
  pretty printer line widths, a la LEGO.  Maybe find a better
  place to do this that in the proof-shell-insert-hook (should
  be triggered by resize events).

*** C Improved configurability of command settings, etc.
  We should let command settings, etc, be a special type
  which can be one of three things:

    'string    -- send this as a command to assistant
    'function  -- call this interactively to return either
		   'string -- send this as a command
		    nil -- do nothing (function does work).
				   
  This way we cover commands which need prompting for extra
  args, as well as elisp functions which do whatever's necessary.
  Then use a generic function "proof-invoke-function" or similar.

*** C Usability enhancement:
   Movement of point after assert/retract commands
    - configure by default for one command/line.
    - Add option for many commands per line.
    - Maybe shell like behaviour with pressing return?

*** C Usability enhancement:
    - Fix proof-script-command-separator and
    proof-one-command-per-line flag, document them.

*** C Support an extended version of dynamic abbreviations, to work
  for commands rather than words.  Should behave a bit like a history
  mechanism in shell buffer: use M-n M-p to scroll up and down
  through previous and forthcoming (matching) commands.

*** C Consider supporting imenu instead, or as well as, func-menu.

*** C Improve proof-easy-config mechanism.   
      
  Let it be redoable by initializing some of the variables to 
  default values to begin with(?).  e.g. proof-script-next-entity-regexps.
  Convention is that everything must be set in proof-easy-config body.
  Use custom to set everything to its default value from proof-config,
  before invoking the body.

*** D Make tags support in lego.el and coq.el a bit more generic.
  Use customization option proof-tags-support.

*** D Display functions: does auto-delete-windows work with
  window-dedicated as it should? (I thought it would switch 
  between 2/3 bufs as appropriate?).

*** D Continue programme of making adaptation easier.  

*** D Fix up sources to conform to library header conventions 
  see (lispref)Library Headers.

*** D Proof shell exit function -- could try sending an interrupt first
  if the process is busy, just to be polite (and avoid the 10 second
  wait before it gets killed).  

*** D X-Symbol: is there a function to input in the minibuffer using
  a token language?

*** D Investigate possible toolbar refresh problems.
  Sometimes extra clicks *are* needed.  Why?

*** D Is there a way to make colours defined for x work in mswindows too?

  defface specs with (type x) seem to work fine with (type mswindows) too.
  Hassle to duplicate, is there an easy way to cover both?

*** C Implement proof-generic-find-and-forget
  <...>-count-undos, to simplify prover-specific code.  
  Complete reengineering of *-count-undos and 
  *-find-and-forget at generic level

*** D Display buffer clearing: response buffer is cleared
  too often/eagerly, perhaps?  The output find-theorems or
  similar doesn't last beyond a single proof step.
  The problem is that we want to erase irrelevant
  output from the response buffer for the previous
  proof step.  Consider making output from invisible
  command persistent.  
  See attempted patch in 
  etc/patches/fix-attempt-for-eager-cleaning.txt

*** C Add to proof-config those variables created in proof-easy-config for
  font lock and syntax entries.  Use these instead of primitive
  elisp in the other configs, too.

*** C Improvements to customization mechanism: watch the use
   of customize-set-variable, odd for users who think it
   means they've changed a setting!
   (currently: next-entity-regexps, proof-splash-settings for Isabelle).

*** C Add improvements to script movement in electric terminator mode.
  Some commented regions in code.  E.g. automatic newline/space after
  C-c C-BS.

*** C Make proof-{script,shell,goals,resp}-font-lock-keywords the
  default way of setting font-lock-keywords, removing from
  proof-easy-config and changing each supported prover instance.

*** D Settings mechanism could be generalised for non-persistent settings

   local settings:
    E.g. Coq has some settings which are local: "Focus" which
    it doesn't make sense to save between sessions or issue
    at the start of the session.
   
   Ideal would be to specify context when local settings are
   relevant, as a predicate.

*** D Modify response display routine a bit to center around recent output,
  or display top, for long output.    Makes better sense for big 
  screen-fulls, perhaps?  Or maybe display top with an itimer to
  move to the bottom after a couple of seconds delay, would be a
  nice effect.

*** D Scheme to detect type of buffer and choose between possible modes.
  Help select Isar over Isa, maybe sml over HOL etc?

*** D Fix the sentinel infinite loop bug which occurs in some cases
  when proof shell startup fails.  Same message is printed over
  and over.  Infinite in GNU Emacs.  Why?  See note at 
  end of proof-shell.  [2hrs]
  

*** D See if there is a way of postponing func-menu loading.

*** D Quit timeout enhancement: instead of killing immediately after
  timeout, could give a message "not responding, kill immediately?"

*** D Consider proof-generic-goal-hyp function, for proof by
  pointing support.  Based on `proof-shell-goal-regexp' which
  I accidently introduced at one point.

*** D Make code robust against accidental deletion of response/goals
  buffer.  Add functions proof-get-or-create-{response,goals}-buffer.
  [30 mins]

*** D proof-script-next-entity-regexps: 
  "However, it does not parse strings, comments, or parentheses."
  Actually we could improve the generic code to ignore
  headings which buffer-syntactic-context suggests are inside
  comments or strings.

*** D Change the name of "automatic multiple files" to something
  more comprehensible.

*** D Strange problem when running in tty mode: c-c c-RET seems to be
  impossible to type.  Consider binding C-c RET instead when
  running on a console.

*** D Tidy up library-loading and dependencies.  (Probably do
  this at the same time as organizing for the XEmacs
  packaging mechanism)

*** D Make compile should give error if any elisp compile fails.

*** D Check support for proof-guess-command-line, new generic setting
  added by Patrick.  Don't know if anyone can use it, actually.

*** D Usability enhancement:
    - Fix asymmetry between "doing" and "undoing": doing will skip comments,
      undoing will not.  e.g. test case: (* tester *) intros; 

*** D Robustify and cleanup code by allowing functions in place of regexps
  for proof-goal-command-regexp and proof-save-command-regexp.
  New names: proof-goal-command-match, proof-save-command-match.
  Then we can remove duplicity and simplify code.

*** D BUGLETS:
  - Response buffer doesn't scroll to display o/p (it does for debug msgs,
    oddly).  This might have been a 1998 design decision.
    Maybe it should be a user option?
  - XEmacs pg forces on font-lock, should it?

*** D SMALL DELTAS:
  - Consider setting proof-mode-for-script automatically?
  Is it ever needed in the shell before the script mode has
  been entered?
  - In case active terminator leads to an error, delete it again?
  (problem synchronizing)
  - Improvements to script navigation commands.  Would like some
  uniformity with proof-find-next-terminator, and a better
  implementation.  Maybe we have four commands: find command start,
  command end, and move to next command/previous command.

*** D Make completion more generic. For Isabelle and Lego, we can build a
  completion table by querying the process, which is better than
  messing with tags.  

*** D outline configuration should be generic  (or else documented for
  each prover separately, since not guaranteed to work for all).

*** D Check matching code carefully, in view of bug reported (now fixed)
  for Isabelle.
  Examine syntax tables for all instances, and whether
  word matching is based on whitespace constituents or non-word
  constituents.  [6 hrs]

*** D Implement proof-auto-retract idea.  [4hrs]

*** D da: Suggested improvement to interface for included files:
  Currently have two cases: processing a single file, and
  retracting which updates the included file list arbitrarily
  (but assumes that only removals are made).  A simpler and
  more general interface would be to just have the second
  case, and automatically find removed files and added files
  between two versions of proof-included-files-list and
  unlock or lock buffers appropriately.  We could provide
  a useful default function based on three regexps:
  retract-file-regexp, add-file-regexp, clear-filelist-regexp.
  Master regexp process-file-regexp would match all of
  these cases.   Could be multiple matches of the three above
  within a single process-file-regexp to avoid processing
  lots of urgent messages.  (3h)

*** D da: goal-hyp: this should be more generic.  At the moment, there are
  generic variables which are only used in the specific code:
  proof-shell-goal-regexp and proof-shell-assumption-regexp.
  This is confusing.  I suggest making lego-goal-hyp the
  default behaviour for proof-goal-hyp-fn a hook function.
  That will work for Isabelle too.   (15 mins)

*** D proof-goal-command-regexp: the syntax of Coq spoils the
   uniform use of a regexp to match a goal (since it allows
   goals to begin Definition ...).  Nonetheless, it would be
   for this not to mean that everyone else needs to set
   proof-goal-command-p.  Perhaps some crucial regexps can
   be used via proof-string-match-p which would allow a 
   function to be invoked instead? (Cf font lock).
   Or via a new generic mechanism for matching or invoking a fn.

*** D ROBUSTness: deal gracefully with possibility that goals buffer is
  killed during session.   (2h)

*** D Add support to filter out unwanted noise from the prover by setting
  up a regular expression  proof-shell-noise-regexp [2hr]

*** D support for templates e.g., in LEGO it would be nice if, by default, 
  fresh buffers corrsponding to file foo.l would automatically insert
  "Module foo;"  Probably by using a generic Emacs package.  [2hr]

*** D Review and prune "FIXME notes" which are notes about ongoing fixes
  or sometimes things to do.  [6hr]

*** D  Write proof-define-derived-mode which automatically adds a 
   call back hook somehow corresponding to our "proof-config-done"
   mess.  Propose this to maintainer of derived.el. (1.5hrs)

*** D Improve proof-goal-command and proof-save-command:
  `proof-goal-command' should be more flexible and support a
  placeholder for the name and the actual goal. In LEGO, we have
    Goal foo : absurd;
    ...
    Save foo;
  Perhaps functions at the generic level to make suitable
  values for the hook, e.g.,

      (setq proof-goal-command  (proof-prompt-named-goal "Goal %s :" "%s;"))

*** D Multiple files: handle failures in reading ancestors.

*** D Provide a sensible default frame/buffer layout (4h)

*** D Implement mouse drag-and-drop support for selecting subterms in the
  goals buffer and copying them in a script buffer. This could be
  implemented by defining button2 in the response buffer and setting
  button2up in script buffers. (1h)

*** D Add support to proof.el for *not* setting variables for
  commands which aren't supported by a prover.  For example,
  in Isabelle there is no such thing as killing a goal.

*** D proof-find-next-terminator is too slow when it needs to parse
  a long buffer.   Generally a performance problem with
  proof-segment-up-to.
  				    
*** D Implement proof-find-previous-terminator and bind it to C-c C-a
  (45min)

*** D Implement a function to undo to the previous goal.

*** D Remove duplication of variables e.g., proof-prog-name and
  lego-prog-name for Coq and Lego. (1h)

*** D More flexible help configuration is needed.  HOL has some nice
  on-line help but no way in PG to help by library.  Perhaps
  a help browser is needed?  At least, optional arg to help command.
  [patch ready and waiting to go in]

*** X Display management is much better than it was, but perhaps
  not quite as good as it could be.  It might be nice to
  display both the goals and response buffer occasionally
  (even with window-dedicated disabled).
  e.g. when proof-shell-erase-response-flag is non-nil
  and the goals buffer is updated: might like to still
  see what was in the response buffer.

*** X Oddities:  
    Response buffer doesn't get cleared after completion
    of a proof followed by retraction of whole file.
    On other cases of retraction, it does.
    Perhaps retraction should set the flag to ensure
    it's cleared.

*** X Making undoing better.
  Rather than calculating an undo command each time an undo command
  is needed, another idea would be to keep the undo command in the
  span.  Then when we amalgamate spans we can construct new undo
  commands.  When we come to issue an undo, we either need to do
  each undo step in turn in reverse, just the final one, or perhaps
  some proof-assistant dependent filtering/modification of the
  set.   At the moment, though, PG is rather keen on issuing just
  one command to forget to some specific place in the script.
  [Maybe a design principle is that spans should coincide with
   undoable regions]

*** X A more flexible way of choosing which instance of PG we want,
    allowing matches on the buffer before choosing the mode function.


** 3. Things to do for the documentation

*** A Doc new bits: proof-next-error

*** A Doc new bits: font lock keywords, filename %e, %r.
  Added proof-{script,shell,goals,resp}-font-lock-keywords.
  Presently used only in proof-easy-config, will put into other
  mechanism

*** A Doc new bits: win32 support

*** A Doc new bits:  settings mechanism via defpacustom 

*** C Update front page image
  - Should include ??? logo to represent other provers

*** B Manual improvements before techreport publishing (see notes at end also):
  - Mention configuring function menus, outline.
  - Consider splitting up chapter 9?
  - document mouse functions, proof-cd, process quit timeout, 
    X-Symbol, prog-name-guess, new menu functions for display.
  - general tips on what to do when things go wrong: try
    interrupt, restart, finally exit proof assistant.
  - improvements after feedback from users.
  - add screenshots?
  - add more index entries

*** B Add something to better document two-buffer versus three-buffer
  interaction modes, and the use of proof-window-dedicated to
  trigger three buffer mode.

*** C Documentation in pdf format: need to fix inclusion of image 
  problem.

*** D Fix INFO-DIR-ENTRY in doc/ProofGeneral.texi to put Proof General 
  info file into a good place.

*** D texi-docstring-magic: first time deffn's, etc, are added, whitespace
  after magic comment is left.

*** B Doc enhancement: explain conditions for switching buffers and auto
  switching of scripting buffers.  (See doc of 
  proof-auto-action-when-switching-scripting)



** 4. Emacs issues

*** GNU Emacs issues

**** A Improve support for Emacs 21.
  X-symbol 4.X fixup for provers other than Isabelle.

**** B Consider replacing buffer-substring -> buffer-substring-no-properties
  Text properties are passed around in spans, probably needlessly.
  (not the same in XEmacs?)

**** C Changed implementation of overlays inside Emacs itself.  We seem to
  need 'priority property of overlays for queue and locked to make 
  sure the colours show through.  Even then highlighting is strange,
  and background face spoils the others.  Transparent?
  Same priority: we get mouse highlighting but no face property.
  Higher priority: we get blanking as mouse highlighting.  Yuk.
  ACTION: check Emacs Lispref for hints.  Maybe ask on newsgroup.

**** X `proof-zap-commas-region' does not work for Emacs 20.4 on
  lego/example.l . On *initially* fontifying the buffer,
  commas are not zapped. However, when entering text (on
  a particular line), commata are zapped correctly. (4h)

*** XEmacs issues

**** C Ask for easy-menu to support :visible keyword
   Very useful option of GNU Emacs easy menu to remove items
   from menu altogether, dynamically.   (Or at least, fairly
   dynamically.  Fully dynamically would be guitrocity).




** 5. Things to do for subterm markup / proof-by-pointing

*** B Unify proof-insert-pbp-command and proof-shell-insert-loopback-cmd.
  Add some debugging messages in proof-done-advancing to indicate
  Maybe pbp should be a new class of "'pbpadvancing" since we don't
  want to allow the flexible queue manipulation here?  Think on it.

*** B Change proof by pointing (pbp) stuff into proofstate buffer stuff.
  Outsource actual pbp/goals functionality 
  (separate pbp annotations from other annotations).
  Rename pbp-mode to response-mode or goals-mode (which doesn't
  support any actual proof-by-pointing), Make a file 
  proof-goals.el.  [4 hrs]

*** C Extend balloon-help (e.g. show pbp command)

*** C Fixing up errors caused by pbp-generated commands; currently, script
  management unwisely assumes that pbp commands cannot fail.
  da: Is this still true?   It looks fine to me.   I think "failure" 
  should mean generates an error.  With LEGO pbp, it uses "Try"
  tactic which always succeeds, whether or not something gets done.

*** C In case of pbp failure (real failure), we might keep a flag
  to indicate that the next pbp command should delete the 
  previous pbp command's insertion into the buffer, to replace
  it with another one.

*** X 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.






** 6. Things to do for Web Pages, Distribution

*** C simplify editing of web pages by instead including files
   with version numbers in them, at least for development version.
   Can also use the link "-latest".

*** C Remove fileshow urls in html

*** D Add an animation, showing proof replay.

*** C Wanted for links: something to UITP.  Are there any pages?

*** C Validate pages.  
   Current failures for HTML 4.0 to do with CGI-style arguments with "&",
   this is a problem with PHP3 really.

*** X Restructure so that page titles are different to help
  browsing.  (Move links_arr from header.html somewhere new,
  and set $pg_title appropriately before head.html is included).

*** X Add some one-stop-shop pages.  Ask permission to redistribute
  packages for PAs.  Maybe do Windows and Linux versions.




** 7. Future improvements to take advantage of newer Emacsen

*** X XEmacs 21.2 compatibility/improvements
**** Accelerators for PG menus?  (how to customize?)
**** Use one-shot-hook for splash display

*** X GNU and XEmacs improvements
**** Indirect Buffers 
  Maybe a cunning way to implement the response buffer and goals
  buffer, since they're basically variants on displaying fragments of
  the shell buffer output. Appears in XEmacs 21.2, GNU 20.5






** 8. Bugs in other software beyond our control

*** A Nasty bug in Emacs 21.{1,2} triggered by
    proof-shell-dont-show-annotations.  Report this.

*** X Code for find-alternate-file has annoying habit of nullifying
    buffer-file-name before kill functions are called, on a buffer
    named ** lose **.  This means PG has to keep a copy of the
    buffer file name to handle proof-included-files-list nicely.
    Would be better if (X)Emacs code didn't do this.

*** X useful if call-process would keep last error state 
      (primarily for exec-to-string, in case of errors)

*** X Odd behaviour of font-lock in script buffers when long strings
contain lines with stuff that looks lisp-ish.  e.g. "(asd . ads)"

*** X oddity: startup delay when running XEmacs remotely and local display
is 8 bit.  Suspect an XEmacs issue to do with face allocations.  Also
huge delay in buffers for Isabelle mode which try to highlight binders
(removed because they appear inside strings anyway)

*** X spurious byte comp warning in XEmacs 21.1.4:
  While compiling proof-x-symbol-encode-shell-input:
     ** buffer-substring called with 3 args, but requires 0-3
  for this code:
               (prog1 (buffer-substring)
                 (kill-buffer (current-buffer))

*** X Error with pdftexinfo (hacked version of teTeX pre-release, 1.0.6).
Gives problem with @value{blah} inside @pdfurl.  May be absent from
pdftexinfo.tex, but that version doesn't seem to generate web links?

*** (/usr/share/texmf.local/pdftex/texinfo/pdftexinfo.tex
Loading texinfo [version 1999-09-25.10]: Basics, pdf,
(/usr/share/texmf/pdftex/plain/misc/pdfcolor.tex) fonts, page headings,
tables, conditionals, indexing, sectioning, toc, environments, defuns, macros,
cross references, (/usr/share/texmf/tex/plain/dvips/epsf.tex) localization,
and turning on texinfo input format.)) (ProofGeneral.aux) [1[/usr/share/texmf/d
vips/config/pdftex.map][/usr/share/texmf.local/dvips/config/dalucida.map][/usr/
share/texmf.local/dvips/adobe/agaramon/pad.map][/usr/share/texmf.local/dvips/co
nfig/wp1.map][/usr/share/texmf.local/dvips/config/mscore.map][/usr/share/texmf.
local/dvips/config/barbedor-ttf.map][/usr/share/texmf.local/dvips/config/goodtt
.map]] [2] (Preface)
! Undefined control sequence.
@indexbreaks ->@catcode `@-=@active @let -
                                          @realdash 
@value ...ode `@-=12 @catcode `@_=12 @indexbreaks 
                                                  @let _@normalunderscore @v...
<argument> @value 
                  {URLpghome}
@pdfurl ...r{/Subtype /Link /A << /S /URI /URI (#1
                                                  ) >>}@endgroup 
@douref ...->@begingroup @unsepspaces @pdfurl {#1}
                                                  @setbox 0 = @hbox {@ignore...
l.264 @uref{@value{URLpghome}}
                              .  Visit this page for
? x
<cmtt10.pfb><cmsy10.pfb><8r.enc><bsfr8a.pfb><bsfc8a.pfb>
Output written on ProofGeneral.pdf (2 pages, 54702 bytes).






   




** 9. New Stable Version Release checklist


***  0. Make all files have same CVS branch with cvs commit -f 
***  1. Tests: multiple file test suites for LEGO, Isabelle; other egs
***  2. Check case with GNU Emacs
***  3. Check case with compiled code, for XEmacs only.
    (Wait for error reports for GNU Emacs)
    Even if the code is faulty afterwards, compiling is 
    worthwhile just because it shows up bugs in unbound variables, etc.
***  4. Dates and versions updated.
        Check README, doc/ProofGeneral.texi, html/download.html, others.
***  5. ProofGeneral.texi docstring magic is up-to-date: cd doc; make magic
***  6. Update Emacs and prover versions in texi, html/ 
***  7. Check web page references from other places.
***  8. Validate web pages if they're changed much.
***  9. Update and distribute etc/announce.  
*** 10. Message to PG mailing list.






** 10. Things to do for Proof General Project


*** A Journal paper on design and development of Proof General.
*** A Grant proposal for Proof General Kit.
*** A Informatics research reports from latest docs.
*** A Small project grant from LFCS for summer student (2003)

*** C PG CDROM: CDROM with PG and other theorem provers 
    Complete read-to-go distributions.  Could make up from TYPES 2002 
    summer school systems to make sure of a consistent set of progs?

*** B Find new people to help advance and develop Proof General.
  Getting more instances is a good way.  Also encouraging feedback.
  Hear stories of bugs by word-of-mouth, they don't get reported often
  enough.

*** A PG projects

*** B PG auxiliary contributions 
	- span library

*** A PG research directions:
	- protocols for interactive proof
	- configuration management / dependency organization
	- ideas about proof engineering cf software engineering
	- research on ways of conducting a formalization, cf
	  ways of writing a program.  Common idioms that PG could
	  help with.


=================================================================

List of things postponed from PG 3.4: need to be merged above

*** Coq pbp focussing --- does this part work at least?  Test case.

*** Comment at the end for Isabelle theory files!!!!

*** X-Symbol 4.4 backwards compatibility for Coq and friends.

*** Check: does proof-follow-mode have any effect???  
    Consider removal to simplify it?

*** Fix-up show/hide for nested proofs.  (Wierdness with
   cursor jumping as well)

*** Cleanup undo behaviour to cope with new Coq mechanism.

 Is the simplified mechanism better for other provers too, or does the
 split still apply?  Probably best to leave Isar as-is and have
 proof-nesting-depth left as experimental.

*** proof-nesting-depth:
    This needs to be fixed up in count undos, find-and-forget.

*** Generic versions of count undos and find-and-forget generic.

*** Keybindings on menus: many missing in GNU Emacs.  
    Also strange things happen with docstrings for macro-generated
    functions.  (C-h C-c C-p gives message "can't find docstring for
    proof-prf" at one point, then later finds it?!)