Nasty things no longer happen, can't load Proof General more than once

2 files changed, 23 insertions, 14 deletions

diff --git a/BUGS b/BUGS
index 9dc47716..2bc22046 100644
--- a/BUGS
+++ b/BUGS
@@ -19,9 +19,10 @@ Workaround: Don't type C-g while script management is processing.  If
 you do, use proof-restart-scripting.
 
 * You can't use more than one proof assistant at a time in the same
-Emacs session.  Nasty things happen if proof-assistants enables
-more than one proof assistant and you load files for different
-provers.  Workaround: stick to one prover per Emacs session!
+Emacs session.  Attempting to load Proof General for a second prover
+will fail.  Workaround: stick to one prover per Emacs session, 
+make sure that the proof-assistants variables only enables 
+Proof General for the provers you need.
 
 * Outline-mode does not work in proof script files due to read-only
 restrictions of protected region.  Workaround: none, nevermind.
diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi
index 1af8d002..bbfd8d73 100644
--- a/doc/NewDoc.texi
+++ b/doc/NewDoc.texi
@@ -202,7 +202,10 @@ Obtaining and Installing Proof General
 @c maybe not in TeX, just put on title page.
 @c not in info, it can't deal with images.
 @c Maybe in HTML because it doesn't appear in titles?
+
+@ifhtml
 @image{ProofGeneral}
+@end ifhtml
 
 @dfn{Proof General} is a generic Emacs interface for proof assistants,
 developed at the LFCS in the University of Edinburgh.
@@ -310,7 +313,7 @@ LEGO Proof General supports all of the generic features of Proof
 General.
 
 See @pxref{LEGO Proof General} for more details.
-@c
+
 @item 
 @b{Coq Proof General} for Coq Version 6.2@*
 @c written by Healfdene Goguen.
@@ -319,7 +322,7 @@ Coq Proof General supports all of the generic features of Proof General
 except multiple files.
 
 See @pxref{Coq Proof General} for more details.
-@c
+
 @item 
 @b{Isabelle Proof General} for Isabelle 98-1@*
 @c written by David Aspinall.
@@ -627,7 +630,8 @@ move the end of the locked region backwards to the end of the segment
 containing the point.
 @end table
 
-Otherwise, you will need to restart script management altogether, @pxref{Toolbar commands}.
+Otherwise, you will need to restart script management altogether,
+@pxref{Toolbar commands}.
 
 
 
@@ -1276,10 +1280,11 @@ details if you don't know where to find this file.
 @unnumberedsubsec Removing support for unwanted provers
 
 You cannot run more than one instance of Proof General at a time: so if
-you're using Coq, don't edit @file{.ML} files!  If there are some
-assistants supported that you never want to use, you can remove them
-from the variable @code{proof-assistants} in @file{proof-site.el} to
-solve this problem.
+you're using Coq, visiting an @file{.ML} file will not load Isabelle
+Proof General, and the buffer remains in fundamental mode.  If there are
+some assistants supported that you never want to use, you can remove
+them from the variable @code{proof-assistants} in @file{proof-site.el}
+to solve this problem.
 
 Via the Customize mechanism, see the menu:
 @example
@@ -1338,11 +1343,14 @@ the system.
 
 @unnumberedsubsec One prover at a time
 You can't use more than one proof assistant at a time in the same Emacs
-session.  Nasty things happen if @code{proof-assistants} enables more
-than one proof assistant and you load script files for different provers
-simultaneously.
+session.  Attempting to load Proof General for a second prover will
+fail, leaving a buffer in fundamental mode instead of the Proof General
+mode for proof scripts.
+
+@strong{Workaround:} stick to one prover per Emacs session, make sure
+that the proof-assistants variables only enables Proof General for the
+provers you need.
 
-@strong{Workaround:} stick to one prover per Emacs session.
 
 @node Bugs specific to LEGO Proof General
 @section Bugs specific to LEGO Proof General