Updated.

4 files changed, 83 insertions, 84 deletions

diff --git a/CHANGES b/CHANGES
index c32572b7..3028a9cb 100644
--- a/CHANGES
+++ b/CHANGES
@@ -137,8 +137,11 @@ Reduce contrast for mouse highlighting of regions.
 *** Added `proof-shell-identifier-under-mouse-cmd'
 
 Allows PG to conveniently send a command to the prover which passes
-the identifier under the mouse as an argument.  Bound globally to
-Control-Meta-Mouse-button1.
+the identifier under the mouse, or the active region, as an argument.
+Bound globally to Control-Meta-Mouse-button1.
+
+Presently only configured in Isabelle/Isar, to parse terms (inside
+strings) and theorems (outside).
 
 
 ** GNU Emacs compatibility, simplified font-lock, handling nested comments
diff --git a/FAQ b/FAQ
index 0a35c69a..32932a34 100644
--- a/FAQ
+++ b/FAQ
@@ -47,7 +47,12 @@ A. This is an XEmacs bug.  What you can do is prevent the use
 
 -----------------------------------------------------------------
 
-Q. I have a problem installing/using Proof General, what can I do?
+Q. I have a problem installing/using Proof General.
+   For example, I see the message
+
+   (file-error "Cannot open load file" "executable")
+
+   when I start the program.
 
 A. Please check the documentation carefully, particularly the
    requirements for a full-featured and recent Emacs version, as
diff --git a/Makefile.devel b/Makefile.devel
index bab65e27..f1499679 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -232,7 +232,7 @@ tags:	$(EL)
 # with a way of cleaning the last day from the ChangeLog.
 #
 ChangeLog:	FORCE
-	rcs2log -h "dcs.ed.ac.uk" $(DEVELOPERS) | sed 's|/home/proofgen/src/ProofGeneral/||g' > ChangeLog.prefix
+	rcs2log -h "dcs.ed.ac.uk" $(DEVELOPERS) -i 4 | sed 's|/home/proofgen/src/ProofGeneral/||g' > ChangeLog.prefix
 	if [ -f ChangeLog ]; then mv ChangeLog ChangeLog.old; else echo > ChangeLog.old; fi
 	cat ChangeLog.prefix ChangeLog.old > ChangeLog
 	rm ChangeLog.prefix ChangeLog.old
diff --git a/todo b/todo
index a529e263..89777919 100644
--- a/todo
+++ b/todo
@@ -6,6 +6,10 @@ This is an outline file.   Use C-c C-n, C-c C-p or menu to navigate.
 
 * Proof General Short List of Things to Do for next version
 
+*** 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)
      -- remove on/off setting for all buffers (too slow), use
@@ -58,50 +62,24 @@ X (Low)		e.g. probably not worth spending time on
 
 *** [ Don't query save before retraction ?? ]
 
-*** A settings configuration for Isabelle: add backwards
-    compatibility for older versions of Isabelle.  
-    Waiting for Isabelle to provide some easy version
-    checking.
-
-*** B Cleanup display during settings processing.
+*** 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 document and simplify proof-script-span-context-menu-extensions
-
-*** C Add output highlighting to minibuffer in proof-shell-message.
-    (Quite tricky to get text properties onto text in minibuffer...)
-
-*** X A more flexible way of choosing which instance of PG we want,
-    allowing matches on the buffer before choosing the mode function.
-
-*** D Isabelle PG: Non-blocking for .thy loading from .ML files.
+*** B Cleanup display during settings processing.
 
 *** B Generic adjusting of pretty-printer line width (currently
     implemented in several instances)
 
-*** D Make code robust against accidental buffer kills
-      by regenerating auxiliary buffers automatically. 
-
-*** 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?
-
-*** C Extensions with semantic tokens
-      Look at the Semantic Navigator package.  Implements persistent
-      database of tokens.
+*** 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.
 
-*** C Fix byte compilation
-      Problem with proof-ass macro mechanism -- gets expanded during compilation.
-
 *** 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.
@@ -110,56 +88,60 @@ X (Low)		e.g. probably not worth spending time on
 
 *** 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)
 
-*** C Fix the doc makefiles to adapt the image flag in PG-adapting.tex
-      properly, for dvi/ps targets
-
-*** B Generalize electric terminator mode for other parsing mechanisms.
+*** B proof-shell-restart should clear response buffer (only noticed with
+  proof-tidy-response=nil)
 
-*** B Add parameter for help function so HOL help works nicely
+*** B TESTING. 
+    - Add automatic testing mechanism to test user-level functions PG
+    - Test schedule for things to try with a new instantiation
 
-*** D Make tags support in lego.el and coq.el a bit more generic.
-  Use customization option proof-tags-support.
+*** 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 ]
 
-*** 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?).
+*** 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!
 
-*** B proof-shell-restart should clear response buffer (only noticed with
-  proof-tidy-response=nil)
-
-*** 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).  
-
 *** 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).
 
-*** 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?
-
-*** C Consider supporting imenu instead, or as well as, func-menu.
-
 *** C Improved configurability of command settings, etc.
   We should let command settings, etc, be a special type
   which can be one of three things:
@@ -188,14 +170,7 @@ X (Low)		e.g. probably not worth spending time on
   mechanism in shell buffer: use M-n M-p to scroll up and down
   through previous and forthcoming (matching) commands.
 
-*** B TESTING. 
-    - Add automatic testing mechanism to test user-level functions PG
-    - Test schedule for things to try with a new instantiation
-
-*** 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 Consider supporting imenu instead, or as well as, func-menu.
 
 *** C Improve proof-easy-config mechanism.   
       
@@ -205,11 +180,32 @@ X (Low)		e.g. probably not worth spending time on
   Use custom to set everything to its default value from proof-config,
   before invoking the body.
 
-*** 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 ]
+*** 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.  
@@ -420,7 +416,6 @@ X (Low)		e.g. probably not worth spending time on
   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)
 
@@ -461,6 +456,8 @@ X (Low)		e.g. probably not worth spending time on
   [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
@@ -752,14 +749,8 @@ Output written on ProofGeneral.pdf (2 pages, 54702 bytes).
 
 List of things postponed from PG 3.4: need to be merged above
 
-*** Stefan Monnier's big patch (Coq stuff, imenu, other)
-
-*** Isar tracing error: (error/warning) Error in process filter: (error Nesting too deep for parser)
-
 *** Coq pbp focussing --- does this part work at least?  Test case.
 
-*** Christophe's changes suggested for handling x-sym / highlighting.
-
 *** Comment at the end for Isabelle theory files!!!!
 
 *** X-Symbol 4.4 backwards compatibility for Coq and friends.