Renamed file

1 files changed, 709 insertions, 0 deletions

diff --git a/TODO.developer b/TODO.developer
new file mode 100644
index 00000000..ced35e65
--- /dev/null
+++ b/TODO.developer
@@ -0,0 +1,709 @@
+-*- mode:outline -*-
+$Id$
+
+This is an outline file.   Use C-c C-n, C-c C-p or menu to navigate.
+
+=================================================================
+
+3.6 TODOs
+=========
+
+* PGIP support
+** Remove need for decorated output around PGIP responses.
+** Support simplified (flat, non context-sensitive) completion for idtables
+** URL parse: library from w3 is incomplete, also may clash with Emacs
+   version.
+
+* X-Symbol
+** Unify versions with distributed XEmacs version
+** Integrate large demo font
+
+* Coq-8 fixup
+** Fix display of sub/super scripts in Coq output
+** Multiple file handling
+** Automatic adjustment of line width
+
+
+=================================================================
+
+* Developers' 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. Long list of things to do in the generic interface
+
+
+*** B Fix-up show/hide for nested proofs.  
+        (Wierdness with cursor jumping as well)
+
+*** B 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.
+
+*** B proof-nesting-depth:
+    This needs to be fixed up in count undos, find-and-forget.
+
+*** C Add MMM for other provers where relevant/useful
+
+*** C Further display management improvement (it's a nightmare)
+    Glitches to resolve:
+     -- suggestion to cache window height: could implement this
+	by resize change functions (also doing the pretty-print hack?)
+        which set a symbol property for associated buffer symbol
+     -- longer term improvements: allow window preferences per 
+	associated buffer.  Either separate frame or merged into
+	switching mode.  Very messy to implement.
+     -- Stuck-withs: XEmacs frames always have minibuffer.
+		     GNU Emacs frames always have modelines.
+     Other older comments:
+      - 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.
+      - check: does auto-delete-windows work with
+      window-dedicated as it should? (I thought it would switch
+      between 2/3 bufs as appropriate?).
+      - 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 Menu layout
+    Would be good to try to make this uniform between version: 
+    PG menu frist, then prover-specific menu.  Similarly for Imenu.
+
+*** A PGIP SUPPORT (minimal for Isabelle patch):
+      -- settings with categories
+
+*** A Oddity: Weirdness with regions turning blue even though they
+    haven't been processed.  Noticed with HOL/CCC experimental setups.
+    Send a few regions queueing, no result from interpreter, yet sometimes
+    turns blue.  Why???
+
+*** C Allow empty retract action that doesn't produce new prompt
+    (Noticed with HOL4).
+
+*** unify format for syntax table entries with imenu (make alist);
+    use config setting for syntax table entries everywhere rather than
+    modify-syntax-entry.
+
+*** C Implement optional arg to next/undo which doesn't update
+      display (so user can retain something else on screen)
+
+*** X Cleanup display during settings processing.
+
+*** C Generic adjusting of pretty-printer line width 
+  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 document and simplify proof-script-span-context-menu-extensions
+
+*** C 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...)
+
+*** B Extensions with semantic tokens
+      Look at the Semantic Navigator package.  Implements persistent
+      database of tokens.
+
+*** 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 ]
+
+*** X 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 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.
+
+  Used e.g. 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.
+
+*** 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 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?
+
+*** X Investigate possible toolbar refresh problems.
+  Sometimes extra clicks *are* needed.  Why?  (Gone in recent Emacsen?)
+
+*** 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
+
+*** 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 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.
+  [1hr]
+
+*** 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.
+
+*** X 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 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).
+
+*** X 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)
+
+*** X Add support to filter out unwanted noise from the prover by setting
+  up a regular expression  proof-shell-noise-regexp [2hr]
+  (any useful examples of noise?)
+
+*** 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.  [6hr]
+
+*** 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 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
+
+*** B New screenshots for web page, also would be nice for manual.
+
+*** B Documentation:
+      Check new doc for hiding; add doc for dependencies, tracing.
+      Moving spans; navigating through locked region.  
+      Favourite menu.
+
+*** 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: difference between GNU Emacs and XEmacs regexps
+  GNU Emacs gives buggy behaviour with "@lisp" regions.
+
+*** 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.
+  To do:  PBP highlighting (?)
+
+**** 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 mouse 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).
+   [NB: this is there now, perhaps, as :configured]
+
+*** A Undo in "read-only" regions 
+
+*** A Support for nested comments
+
+
+
+** 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.  
+
+*** 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 Error with pdftexinfo (still there?) 
+Gives problem with @value{blah} inside @pdfurl.  May be absent from
+pdftexinfo.tex, but that version doesn't seem to generate web links?
+
+
+
+
+** 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 for compiler warnings running "make", on XEmacs & Emacs
+***  3. Test cases using compiled code on Emacs and XEmacs.
+***  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 grants for summer students
+*** A Small project grant from LFCS for summer student
+
+*** B "Spam-protect" (ho, ho) email addresses on web pages
+*** B Fixup HTML on mailing list pages (image address)
+
+*** 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 always by word-of-mouth, they don't get
+     reported often enough by email.
+*** A PG student projects
+*** B PG auxiliary contributions 
+*** C PG CDROM: CDROM with PG and other theorem provers.  Useful?
+