Updated.

1 files changed, 189 insertions, 216 deletions

diff --git a/FAQ b/FAQ
index 06320165..c27f8094 100644
--- a/FAQ
+++ b/FAQ
@@ -8,348 +8,321 @@ Please also check the BUGS file.
 
 -----------------------------------------------------------------
 
-Q. Proof General fails to load with an error message on start-up: 
- 
-      Proof General was compiled for GNU Emacs 22.1 but running on XEmacs 21.5: please run "make clean; make"
+Q1. Proof General fails to load with an error message on start-up,
+    containing text like this: 
+  
+       Proof General was compiled for GNU Emacs 22.1 but 
+       running on XEmacs 21.5: please run "make clean; make"
 
-   or
+    or
 
-     error: "File `.../ProofGeneral/generic/proof-autoloads.elc' was 
-     not compiled in Emacs"
+      error: "File `.../ProofGeneral/generic/proof-autoloads.elc' was 
+      not compiled in Emacs"
 
-   What's wrong?
+    What's wrong?
 
-A. We distribute compiled .elcs for GNU Emacs 22.1, so you will have to
-   delete them and (optionally) recompile for your preferred 
-   Emacs version.  Using the Makefile:
+A1. We distribute compiled .elcs for GNU Emacs 22.1, so you will have to
+    delete them and (optionally) recompile for your preferred 
+    Emacs version.  Using the Makefile:
 
      make clean			#   removes all .elc files.  
 
-   and then a command like this:
+    and then a command like this:
 
      make EMACS=xemacs
 
-   Note: GNU Emacs is recommended.  XEmacs support may be removed 
-   in future.
+    Note: GNU Emacs is recommended.  XEmacs support may be removed 
+    in future.
 
    
 
 -----------------------------------------------------------------
 
-Q. Proof General fails to load with an error message like this: 
+Q2. Proof General fails to load with an error message like this: 
 
      file mode specification error: 
 	(file-error "cannot open load file" "executable")
 
-   What's wrong?
+    What's wrong?
+
+A2. You're missing some Emacs (probably XEmacs) packages.  See
+    the section "Dependency on Other Emacs Packages" in INSTALL.
+    Quicker answer: install the "XEmacs Sumo" package collection.
+
 
-A. You're missing some Emacs (probably XEmacs) packages.  See
-   the section "Dependency on Other Emacs Packages" in INSTALL.
-   Quicker answer: install the "XEmacs Sumo" package collection.
 
 -----------------------------------------------------------------
 
-Q. Emacs appears to hang when the prover process is started.
+Q2. Emacs appears to hang when the prover process is started.
 
-A. This is usually caused by UTF-8 support in recent linuxes with
-   Glibc 2.2 or later, probably enabled with UTF8 encoded output in
-   your default locale.  Unfortunately Proof General traditionally
-   relied on 8-bit characters which are UTF8 prefixes in the output of
-   proof assistants (inc Coq, Isabelle).  These prefix characters are
-   not flushed to stdout individually.  As a workaround we can disable
-   interpretation of UTF8 in the C libraries.
+A2. This is usually caused by UTF-8 support in recent linuxes with
+    Glibc 2.2 or later, probably enabled with UTF8 encoded output in
+    your default locale.  Unfortunately Proof General traditionally
+    relied on 8-bit characters which are UTF8 prefixes in the output of
+    proof assistants (inc Coq, Isabelle).  These prefix characters are
+    not flushed to stdout individually.  As a workaround we can disable
+    interpretation of UTF8 in the C libraries.
 
-   Doing this inside PG/Emacs is unreliable; locale settings are
-   set/inherited in strange ways.  One solution is to run the Emacs
-   process itself with an altered locale setting, e.g., 
+    Doing this inside PG/Emacs is unreliable; locale settings are
+    set/inherited in strange ways.  One solution is to run the Emacs
+    process itself with an altered locale setting, e.g., 
 
-   $  LC_CTYPE=en_GB xemacs &
+    $  LC_CTYPE=en_GB xemacs &
 
-   (where $ is the shell prompt; this example is for my locale which
-    by default is "en_GB.UTF-8": I see this by typing "locale" at
-    the prompt).
+    (where $ is the shell prompt; this example is for my locale which
+     by default is "en_GB.UTF-8": I see this by typing "locale" at
+     the prompt).
 
-   (This fix is attempted in the supplied "proofgeneral" script, as
-    well as making an adjustment in Proof General when the string UTF
-    appears in the current value of LC_CTYPE).
+    (This fix is attempted in the supplied "proofgeneral" script, as
+     well as making an adjustment in Proof General when the string UTF
+     appears in the current value of LC_CTYPE).
 
-   Alternatively you can set LC_CTYPE inside a file ~/.i18n, which will
-   be read the shell.  Put a line such as "LC_CTYPE=en_GB" into this file.
-   However, this action will affect all applications.
+    Alternatively you can set LC_CTYPE inside a file ~/.i18n, which will
+    be read the shell.  Put a line such as "LC_CTYPE=en_GB" into this file.
+    However, this action will affect all applications.
 
-   NB: a related issue is warnings from x-symbol: "Emacs language 
-   environment and system locale specify different encoding, I'll 
-   assume `iso-8859-1'".  This warning appears to be mostly harmless.
-   Notice that the variable `buffer-file-coding-system' may determine
-   the format that files are saved in.  
+    NB: a related issue is warnings from x-symbol: "Emacs language 
+    environment and system locale specify different encoding, I'll 
+    assume `iso-8859-1'".  This warning appears to be mostly harmless.
+    Notice that the variable `buffer-file-coding-system' may determine
+    the format that files are saved in.  
 
-   Another way to affect this which has been suggested is to add a line
-   like this to the init.el file on XEmacs:
+    Another way to affect this which has been suggested is to add a line
+    like this to the init.el file on XEmacs:
   
-     (prefer-coding-system 'ctext)
+      (prefer-coding-system 'ctext)
 
-   but I haven't tried this.
+    but I haven't tried this.
 
-   ** Update for PG 3.7 **
+    ** Update for PG 3.7 **
 
-   The above fixes should not be necessary with most recent prover
-   versions.  Isabelle 2007 has a "Unicode-safe" interaction mode,
-   enabled by default (to disable, customise `proof-shell-unicode').
-   This is also used by the Isabelle startup scripts.  Coq 8.1 and
-   later do not use non-ASCII characters in output.
+    The above fixes should not be necessary with most recent prover
+    versions.  Isabelle 2007 has a "Unicode-safe" interaction mode,
+    enabled by default (to disable, customise `proof-shell-unicode').
+    This is also used by the Isabelle startup scripts.  Coq 8.1 and
+    later do not use non-ASCII characters in output.
 
   
 
 -----------------------------------------------------------------
 
-Q. Proof General shows a warning like this when started:
+Q3. Help, I'm stuck!! Emacs keeps telling me "Cannot switch buffers in a
+    dedicated window"  
 
-      (1) (file-mode-spec/warning) Error in File mode specification: Invalid argument: Invalid tag set, (mule-fonts)
+A3. This can happen if you enabled "Use Three Panes" and then change
+    the panes (window) layout manually, typically by deleting another 
+    window or frame so you only have a "dedicated" window on the 
+    display.  Don't kill Emacs!  There are many ways of getting out,
+    e.g.
+    -- In single window mode, C-c C-l (proof-layout-windows) refreshes
+       the display
 
-  Backtrace follows:
+    -- In multiple window mode, if you have accidently deleted the main
+       window, get a new one with M-x new-frame RET
 
-    canonicalize-tag-set((mule-fonts))
-
-   Also/alternatively, I notice junk in the output display with funny
-   accented characters.  What's wrong?
-
-A. You're probably using a 21.5.x beta version of XEmacs which is
-   incompatible with X-Symbol (both the version distributed with
-   XEmacs and the version distributed with Proof General).  
-   Please update to a 2007 development release of Proof General
-   which has added some compatibility patches for XEmacs 21.5.
 
 
 -----------------------------------------------------------------
 
-Q. Help, I'm stuck!! Emacs keeps telling me "Cannot switch buffers in a
-   dedicated window"  
+Q4. XEmacs displays a progress bar during fontification which
+    sometimes gets stuck or messes up the display.  
+    Is this a Proof General bug?  What can I do?
 
-A. This can happen if you enabled "Use Three Panes" and then change
-   the panes (window) layout manually, typically by deleting another 
-   window or frame so you only have a "dedicated" window on the 
-   display.  Don't kill Emacs!  There are many ways of getting out,
-   e.g.
-   -- In single window mode, C-c C-l (proof-layout-windows) refreshes
-      the display
+A4. This is an XEmacs issue.  You can prevent the use of the ugly
+    widget, for example by adding
 
-   -- In multiple window mode, if you have accidently deleted the main
-      window, get a new one with M-x new-frame RET
+     (setq progress-feedback-use-echo-area t)
 
------------------------------------------------------------------
+    inside your configuration file `.xemacs/init.el'.
 
-Q. XEmacs appears to hang on certain malformed inputs to the prover.
 
-A. This symptom may be caused by using non-Mule versions of XEmacs.
-   Please make sure you use a Mule-enabled version.
 
 -----------------------------------------------------------------
 
-Q. XEmacs 21.4 displays a progress bar during fontification which
-   sometimes gets stuck or messes up the display.  
-   Is this a Proof General bug?  What can I do?
+Q5. I have a problem installing/using Proof General, what can I do?
 
-A. This is an XEmacs bug.  Things are better in morea recent patches 
-   of 21.4, make sure you have the latest version.  You can prevent
-   the use of the ugly widget, for example by adding 
+A5. Please check the documentation carefully, particularly the
+    requirements for a full-featured and recent Emacs version, as
+    mentioned in INSTALL (see "Dependency on Other Emacs Packages").  
+    If you still cannot solve your problem, try to contact someone
+    else who is using Proof General with a similar setup.  The
+    best way to do this may be through the user mailing list for your
+    proof assistant.  If you think the problem is Proof General related,
+    consult the PG Wiki and Trac pages.
 
-     (setq progress-feedback-use-echo-area t)
 
-   inside your configuration file `.xemacs/init.el'.
 
 -----------------------------------------------------------------
 
-Q. I have a problem installing/using Proof General, what can I do?
-
-A. Please check the documentation carefully, particularly the
-   requirements for a full-featured and recent Emacs version, as
-   mentioned in INSTALL (see "Dependency on Other Emacs Packages").  
-   If you still cannot solve your problem, send a message to
-   da+pg-support@inf.ed.ac.uk in the first instance.
+Q6. I'm using Proof General for prover X, then I load a file for
+    prover Y.  I get an error.  Why?
 
------------------------------------------------------------------
+A6. Unfortunately the architecture of Proof General is designed so
+    that you can only use one prover at a time in the same Emacs
+    session.   If you want to run more than one prover at a time,
+    you have to run more than one Emacs.
 
-Q. I'm using Proof General for prover X, then I load a file for prover Y.
-   The buffer doesn't enter the mode for prover Y.  Why not?
 
-A. Unfortunately the architecture of Proof General is designed so
-   that you can only use one prover at a time in the same Emacs
-   session.   If you want to run more than one prover at a time,
-   you have to run more than one Emacs.
 
 -----------------------------------------------------------------
 
-Q. I have just installed Emacs, ProofGeneral and a proof assistant.
-   It works but X-Symbol is not being activated.
+Q7. I have just installed Emacs, ProofGeneral and a proof assistant.
+    It works but X-Symbol is not being activated.
 
-A. Once X-Symbol is picked up by Emacs (e.g. is working for TeX), 
-   you should enable it inside Proof General by the menu item:
+A7. Once X-Symbol is picked up by Emacs (e.g. is working for TeX), 
+    you should enable it inside Proof General by the menu item:
 
-     Proof-General -> Options -> X-Symbol
+      Proof-General -> Options -> X-Symbol
   
-   To enable it automatically every time you use Proof General,
-   type
-
-        M-x customize-variable RET isar-x-symbol-enable RET
-
-   and change/set/save the setting to `on'.  
-
-   Note that we don't do this by default, because from the system's
-   perspective it is difficult to determine if this will succeed ---
-   or just produce funny characters that confuse new users even more.
-
-   If you are using Isabelle, the wrapper script will load X-Symbol
-   from any location, and you can enable it by passing the option 
-   "-x true".
+    To enable it automatically every time you use Proof General,
+    type
 
------------------------------------------------------------------
-
-Q. I notice that editing Isabelle files in Proof General with XEmacs
-   21.4 is very slow.  Can this be fixed?
+         M-x customize-variable RET isar-x-symbol-enable RET
+ 
+    and change/set/save the setting to `on'.  
 
-A. You could consider adding the following line to your init file:
+    Note that we don't do this by default, because from the system's
+    perspective it is difficult to determine if this will succeed ---
+    or just produce funny characters that confuse new users even more.
 
-      (setq lookup-syntax-properties nil)
+    If you are using Isabelle, the wrapper script will load X-Symbol
+    from any location, and you can enable it by passing the option 
+    "-x true".
 
-   This hack bypasses some very slow code in the font-lock system, but
-   it also disables some syntax-related features, so use with care.
 
 -----------------------------------------------------------------
 
 
-Q. I'm afraid I got stuck very early on.  I sent the following line:
+Q8. I'm afraid I got stuck very early on.  I sent the following line:
 
       by (swap_res_tac [psubsetI] 1;
 
-   Notice that I forgot the right bracket.  The line went pink, the
-   buffer went read-only and nothing I tried would let me fix the
-   error.  
-
-A. The proof process is waiting for more input because of the missing
-   parenthesis, but Proof General doesn't realise this and waits for a
-   response.  You should type something in the proof shell, or
-   interrupt the process with C-c C-c or the Stop button.
+    Notice that I forgot the right bracket.  The line went pink, the
+    buffer went read-only and nothing I tried would let me fix the
+    error.  
 
------------------------------------------------------------------
-
-Q. How can I keep the Proof General option settings across sessions?
+A8. The proof process is waiting for more input because of the missing
+    parenthesis, but Proof General doesn't realise this and waits for a
+    response.  You should type something in the proof shell buffer
+    (*isabelle*), or interrupt the process with C-c C-c or the Stop button.
 
-A. For options set in the Proof General -> Options menu use the 
-   "Save Options" menu item (Proof General -> Options -> Save Options).
-
-   For other options set via customize (Proof General -> Advanced -> 
-   Customize), use the customize buttons, or M-x customize-save-customized.
 
 -----------------------------------------------------------------
 
-Q. How do I use Proof General for Isabelle classic instead of Isabelle/Isar?
-
-A. There are several ways:
+Q9. How can I keep the Proof General option settings across sessions?
 
-   1. Use the Isabelle settings mechanism, invoke with "Isabelle"
-   2. Set the environment variable PROOFGENERAL_ASSISTANTS=isa
-      before starting Emacs.
-   3. Put the line (* -*- isa -*- *) at the top of your files.
+A9. For options set in the Proof General -> Options menu use the 
+    "Save Options" menu item (Proof General -> Options -> Save Options).
 
-   Unfortunately Isabelle/Isar and Isabelle classic are two quite
-   separate Proof General instances.  Ideally they should be
-   combined into one, if anyone fancies some elisp hacking...
+    For other options set via customize (Proof General -> Advanced -> 
+    Customize), use the customize buttons, or M-x customize-save-customized.
 
 
 -----------------------------------------------------------------
 
-Q. When using X-Symbol, why do I sometimes see funny characters like
-   \233 in the buffer?
+Q10. When using X-Symbol, why do I sometimes see funny characters like
+    \233 in the buffer?
 
-A. These are part of the 8 bit character codes used by X Symbol to
-   get symbols from particular fonts.  Sometimes X-Symbol forgets to
-   fontify the buffer properly to make it use the right fonts.
-   (That's being rather unkind to X-Symbol: several things can 
-    go wrong one way or another).
+A10. These are part of the 8 bit character codes used by X Symbol to
+     get symbols from particular fonts.  Sometimes X-Symbol forgets to
+     fontify the buffer properly to make it use the right fonts.
+     (That's being rather unkind to X-Symbol: several things can 
+      go wrong one way or another).
 
-   To fix, type 
+     To fix, type 
 
-	M-x x-symbol-decode-recode
+  	M-x x-symbol-decode-recode
 
-   If that doesn't work, type M-x font-lock-mode twice to turn font-lock 
-   off then on.   Or reload the file.
-   
-   Note that X-Symbol is more robust when used with XEmacs/Mule.
+     If that doesn't work, type M-x font-lock-mode twice to turn
+     font-lock off then on.  Or reload the file.
+     
+     Read the X-Symbol documentation for (much) more information.
+     http://x-symbol.sourceforge.net/man/
 
-   Read the X-Symbol documentation for (much) more information.
-   http://x-symbol.sourceforge.net/man/
 
 -----------------------------------------------------------------
 
-Q. I would like to use the X-Symbol fonts in PG not just at the
-   standard size but also for larger sizes since I use PG during
-   talks, where I set the font size to 24.
+Q11. I would like to use the X-Symbol fonts in PG not just at the
+     standard size but also for larger sizes since I use PG during
+     talks, where I set the font size to 24.
+
+A11. There are X-Symbol fonts at sizes of 12, 14, 18 and 24.  The
+     standard size is 14, and 12 is used for subscripts.  The font size
+     can be changed by adding
 
-A. There are X-Symbol fonts at sizes of 12, 14, 18 and 24.  The standard size
-   is 14, and 12 is used for subscripts.  The font size can be changed by
-   adding
+	(setq x-symbol-font-sizes '(("" 24 18)))
 
-  (setq x-symbol-font-sizes '(("" 24 18)))
+     to your .emacs, which causes the special fonts to come up in size
+     24 and 18 for subscripts; the normal font can be changed
+     manually.  By choosing other sizes, it is also possible to scale
+     the existing fonts.  Note that the larger fonts are not perfect.
 
-   to your .emacs, which causes the special fonts to come up in size
-   24 and 18 for subscripts; the normal font can be changed manually.  By
-   choosing other sizes, it is also possible to scale the existing fonts.
-   Note that the larger fonts are not perfect.
+     If you use Isabelle (both isa or isar) you can specify the
+     X-Symbol font size through the -f option of the start-up-script.
+     The size is passed to emacs through the environment variable
+     XSYMBOL_FONTSIZE, which can be used to configure the normal font in
+     your .emacs.
+
+     You can also use X-Symbol with scalable fonts rather than
+     the default bitmaps.  This is the mechanism used for Mac and
+     would work for GNU Emacs >=23 versions, but there isn't yet
+     a way to configure this automatically.
 
-   If you use Isabelle (both isa or isar) you can specify the X-Symbol font
-   size through the -f option of the start-up-script.  The size is passed to
-   emacs through the environment variable XSYMBOL_FONTSIZE, which can be used
-   to configure the normal font in your .emacs.
 
 -----------------------------------------------------------------
 
-Q. The "Favourites" feature to insert/send fixed strings is great, 
-   but I'd like to define a command which takes arguments.
+Q12. The "Favourites" feature to insert/send fixed strings is great, 
+     but I'd like to define a command which takes arguments.
 
-A. You can do that in Elisp with a command like this: 
+A12. You can do that in Elisp with a command like this: 
 
-    (proof-definvisible isar-theorem
-      '(format "thm %s" (read-string "theorem: "))
-       [(control t)])
+      (proof-definvisible isar-theorem
+        '(format "thm %s" (read-string "theorem: "))
+         [(control t)])
 
-   (NB: it binds the key C-c C-a C-t).  See the documentation for
-   `proof-definvisible' and `proof-defshortcut`.
+     (NB: it binds the key C-c C-a C-t).  See the documentation for
+     `proof-definvisible' and `proof-defshortcut`.
 
 
 -----------------------------------------------------------------
 
-Q. Why do I get a warning "Bad version of xml.el found, ..."?
+Q13. Why do I get a warning "Bad version of xml.el found, ..."?
 
-A. Your Emacs distribution includes a version of xml.el which has 
-   fundamental bugs.   The patched version of xml.el, in lib/xml-fixed.el
-   has been loaded instead.  This works for Proof General because it fixes
-   the basic bugs, but it may cause compatibility issues in other packages
-   (e.g. it is quite different from the latest xml.el with GNU Emacs
-   development versions).
+A13. Your Emacs distribution includes a version of xml.el which has 
+     fundamental bugs.   The patched version of xml.el, in lib/xml-fixed.el
+     has been loaded instead.  This works for Proof General because it fixes
+     the basic bugs, but it may cause compatibility issues in other packages
+     (e.g. it is quite different from the latest xml.el with GNU Emacs
+     development versions).
    
-   This message is probably nothing to worry about unless you are using
-   the same Emacs session for other packages that heavily use xml.el
-   (e.g. GNUS).
+     This message is probably nothing to worry about unless you are using
+     the same Emacs session for other packages that heavily use xml.el
+     (e.g. GNUS).
+
 
 -----------------------------------------------------------------
 
-Q. I see spurious ^M characters at the end of lines in the 
-   windows showing output from the prover.  How can I remove
-   them?
+Q14. I see spurious ^M characters at the end of lines in the 
+     windows showing output from the prover.  How can I remove
+     them?
+
+A14. Customize the value of `proof-shell-strip-crs-from-output'.
 
-A. Customize the value of `proof-shell-strip-crs-from-output'.
 
 -----------------------------------------------------------------
 
 
-Q. Can I join any mailing lists for Proof General?
+Q15. Can I join any mailing lists for Proof General?
+
+A15. Of course, email "proofgeneral-request@informatics.ed.ac.uk" 
+     with the line "subscribe" in the message body, to join the
+     users' and announcements list.
+
+     There is also a list for developers, proofgeneral-devel:
 
-A. Of course, email "proofgeneral-request@informatics.ed.ac.uk" 
-   with the line "subscribe" in the message body, to join the
-   users' and announcements list.
+        http://proofgeneral.inf.ed.ac.uk/mailinglist 
 
-   There is also a list for developers, proofgeneral-devel
-   Visit http://proofgeneral.inf.ed.ac.uk/mailinglist for more details.
+     for more details.