Updated.

4 files changed, 42 insertions, 117 deletions

diff --git a/BUGS b/BUGS
index a3bd4083..b9f3c4d6 100644
--- a/BUGS
+++ b/BUGS
@@ -3,12 +3,10 @@
 * Known Bugs and Workarounds for Proof General.
 
 For latest, see: http://proofgeneral.inf.ed.ac.uk/trac
-
 See also FAQ:    http://proofgeneral.inf.ed.ac.uk/FAQ
 
 Generic bugs are listed here, which may affect all of the supported
-provers.  See lego/BUGS coq/BUGS, etc, for specific bug lists for each
-of the provers supported.  
+provers.  See lego/BUGS coq/BUGS, etc, for a few specific bugs.
 
 The bugs here are split into problems which apply for all Emacs
 versions, and those which only apply to particular versions.
@@ -18,24 +16,14 @@ PG are mentioned in the FAQ.
 
 * Reporting bugs
 
-If you have a problem that is not mentioned here, please contact me at
-the address above.  Please describe your problem carefully, include a
-short demonstration file and tell me the exact version of Emacs and
-Proof General that you are using.  You can use the menu command
-
-  Proof General -> Help -> Send Bug Report
-
-to conveniently include the proper version numbers in your message.
+If you have a problem that is not mentioned here, please visit the
+Trac at the address above to add a ticket.  Please describe your
+problem carefully, include a short demonstration file and tell us the
+exact version of Emacs and Proof General that you are using.
 
 
 * Generic problems, for all Emacs versions
 
-** X-Symbol support removed from "secondary" provers (HOL, ACL2, LEGO, Twelf)
-
-If anyone was actually using this, please let me know.  It should be
-very easy to revive by copying coq/x-symbol-coq.el (although a generic
-version might be desirable).
-
 ** Visibility control doesn't distinguish theorems with same name.
 
 If you have more than one theorem with the same name in a buffer,
@@ -101,8 +89,7 @@ If you do, use proof-restart-scripting to be sure of synchronizing.
 Because of read-only restrictions of the protected region.  
 This is an inherent problem with outline because it works by 
 modifying the buffer.
-Workaround: none, nevermind.  (If it's hugely needed we could support
-modified outline commands).
+Workaround: none.  
 
 ** When proof-rsh-command is set to "ssh host", C-c C-c broken
 
@@ -136,7 +123,7 @@ bug which may be Emacs-related: from now on I will add a note here
 rather than try to investigate older Emacsen and add more patches 
 to the code.
 
-** XEmacs "nesting too deep for parser" warnings (unresolved in any XEmacs)
+** XEmacs "nesting too deep for parser" warnings
 
 This is sometimes triggered by very complex output, typically with
 Isabelle's tracing messages when font-lock is called. 
@@ -161,30 +148,8 @@ been changed on the file system you see the error:
 
 As a result fontification, etc, fails. Workaround: use C-x C-v
 instead.  This problem has gone away since 21.4.12 or so.
-
 Update: this has reappeared in version 21.4.15.
 
-
-** GNU Emacs menus: options not updated dynamically, positions erratic, etc.
-
-Also, proof assistant specific menus only appear in scripting buffer.
-These are drawbacks with GNU Emacs menu support on early versions.  As
-of Emacs 21.3, these glitches have gone.  (Although bugs have been
-known to return).
-
-** GNU Emacs faces sometimes faulty, esp in console mode
-
-Emacs support is let down in console mode, because faces are not
-implemented there.  (XEmacs can use colours and underline in console
-mode)
-
-** If you have problems using Mule versions of GNU Emacs 
-
-Beware setting standard-display-european: Pascal Brisset suggests
-adding this line to .emacs should help:
-
-   (setq process-coding-system-alist '(("" . no-conversion))) 
-
 ** XEmacs undo in the script buffer can edit the "uneditable region"
 
 Test case: Insert some nonsense text after the locked region.
@@ -192,41 +157,3 @@ Kill the line. Process to the next command.
 Press C-x u, nonsense text appears in locked region.
 Workaround: take care with undo in XEmacs.
 
-** X-Symbol on GNU Emacs
-
-X-Symbol 4.X isn't finished yet and will only supported GNU Emacs from
-GNU Emacs 21.4 onwards.  For the time being there are a few minor
-glitches (buffer gets modified during decoding,
-subscripts/superscripts don't work, output colouration may spill into
-adjacent symbols...), but on the whole it is quite usable (and
-rather faster than XEmacs).  For more information about X-Symbol,
-see http://x-symbol.sourceforge.net.
-
-** As of GNU Emacs 20.3, multi-byte character codes are used.  
-
-This breaks some of the code in Proof General, which is turned off in
-case the suspicious looking function
-toggle-enable-multibyte-characters is present.  The code that is
-turned off deals with term markup for proof by pointing, which only
-affects LEGO at the moment.  This problem could affect forthcoming
-versions of XEmacs (but hasn't as far as XEmacs 21.4).  [Can anybody
-tell us if it affects Mule versions of Emacs?]  
-
-Workaround: for LEGO pbp, use GNU Emacs 20.2, or XEmacs 20.4/later.
-
-** XEmacs sometimes has strange start-up delays of several seconds.
-
-Possibly due to face allocation, when running remotely and
-displaying on an 8-bit display.  One workaround (and in fact the
-recommended way of working) is to run XEmacs locally and only
-the proof assistant on your fast compute server, by setting 
-proof-rsh-command.
-
-** Looping in Emacs 21.2
-
-Several (odd) circumstances cause this version of Emacs to loop,
-in particular, when moving the cursor into multi-byte characters.
-Workarounds have been added to avoid this: you may see junk
-characters in the shell buffer as a side effect. 
-
-
diff --git a/COMPATIBILITY b/COMPATIBILITY
index 64af7b6c..819a9299 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -10,11 +10,10 @@ on Linux:
  XEmacs 21.5 (beta28)  -- tested; PG has workarounds for several bugs
  XEmacs 21.4.XX	       -- tested
 
-and prover versions:
+and (main) prover versions:
 
- Coq 8.1
- Isabelle2005
- Isabelle2007
+ Coq 8.0, 8.1
+ Isabelle2005, Isabelle2007
 
 Maintaining compatibility across proof assistant versions, Emacs
 versions and operating systems is a big challenge!  Please visit this
diff --git a/INSTALL b/INSTALL
index 542df03a..d008216a 100644
--- a/INSTALL
+++ b/INSTALL
@@ -32,7 +32,7 @@ If none of these files help, then contact me via the address below.
    University of Edinburgh.
    Edinburgh.
    
-   http://proofgeneral.inf.ed.ac.uk
+   http://proofgeneral.inf.ed.ac.uk/trac
 
 
 
@@ -91,11 +91,14 @@ to your .emacs file.
 Running on Windows
 ------------------
 
+For tips, please see here:
+
+http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGEmacsOnWindows
+
 Note that Windows compatibility isn't tested by the maintainers.  If
 you discover problems, please send a fix to the address above.
 
-We recommend XEmacs compiled for Windows, see http://www.xemacs.org.
-Some Isabelle users have reported better operation with cygwin XEmacs.
+We recommend EmacsW32 http://www.ourcomments.org/Emacs/EmacsW32.html
 
 Unpack the Proof General tar or zip file, and rename the folder to
 "ProofGeneral" to remove the version number.  Put a line like this:
@@ -103,26 +106,34 @@ Unpack the Proof General tar or zip file, and rename the folder to
    (load-file "c:\\ProofGeneral\\generic\\proof-site.el")
 
 into .emacs.  You should put .emacs in value of HOME if you set that,
-or else in directory you installled XEmacs in, e.g.  
-c:\Program Files\XEmacs\.emacs
+or else in directory you installled Emacs in, e.g.  
+c:\Program Files\Emacs\.emacs
 
 
 Running on Mac OS X
 -------------------
 
-Larry Paulson maintains a web page on running Isabelle on Mac OS X
-which includes instructions for using Proof General in that
-environment.  See here:
+Please see here:
+
+http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGEmacsOnMacOSX
+
 
-   http://www.cl.cam.ac.uk/Research/HVG/Isabelle/macosx.html
 
-His brief summary is:
- 
-  1. Install X11 or OroborOSX.
-  2. Install XEmacs, or install GNU Emacs and recompile Proof General.
+Byte Compilation.
+-----------------
+
+Compilation of the Emacs lisp files improves efficiency but can
+sometimes cause compatibility problems.  In particular, byte compiled
+files are generally not compatible between XEmacs and GNU Emacs.
+
+We distribute .elcs for GNU Emacs, so you will have to delete
+them and (optionally) recompile for XEmacs.
+
+Use 'make clean' to remove all .elc files.  
+Use 'make compile' to recompile .elc files.
+
+Check that the Makefile sets EMACS to your Emacs executable.
 
-If you use XEmacs bear in mind the note below (if you are using fink,
-install xemacs-sumo-pkg).
 
 
 Dependency on Other Emacs Packages
@@ -153,21 +164,6 @@ do not need to download it separately.
 
 
 
-Byte Compilation.
------------------
-
-Compilation of the Emacs lisp files improves efficiency but can
-sometimes cause compatibility problems.  In particular, byte compiled
-files are generally not compatible between XEmacs and GNU Emacs.
-
-We distribute .elcs for XEmacs, so you will have to delete
-them and (optionally) recompile for GNU Emacs.
-
-Use 'make clean' to remove all .elc files.  
-Use 'make compile' to recompile .elc files.
-
-Check that the Makefile sets EMACS to your Emacs executable.
-
 
 Site-wide Installation
 ----------------------
diff --git a/README b/README
index a04c7346..bccca6fa 100644
--- a/README
+++ b/README
@@ -1,12 +1,13 @@
 	    Proof General --- Organize your proofs! 
 
 Proof General is a generic Emacs interface for proof assistants.
-
-This is version 3.7 of Proof General (see about screen for exact version).   
-
 The aim of the Proof General project is to provide a powerful, generic
 environment for using interactive proof assistants.
 
+This is version 3.7 of Proof General. 
+(see About screen for exact version).   
+
+
 See
     INSTALL	   for installation details.
     COPYING	   for license details.
@@ -38,12 +39,14 @@ in the subdirectories:
 
  generic/   Generic basis for Proof General
 
+
 A small number of example proofs are included in each prover 
 subdirectory.   The "root2" example proofs of the irrationality
 of the square root of 2 were proofs written as a response
 to a challenge of Freek Wiedijk in his comparison of different
 theorem provers, see http://www.cs.kun.nl/~freek/comparison/.
 Those proof scripts are copyright by their named authors.
+(NB: some of these may have rusted)
 
 Check BUGS files for problems and issues.  Please report new bugs
 on the Trac site at http://proofgeneral.inf.ed.ac.uk/trac.