# HG changeset patch
# User wenzelm
# Date 1359200732 -3600
# Node ID d6de6e81574d4e3e0ef847c68d241252d95c59d3
# Parent  81a75d9a9a4eb6a03a144a4df771f6c6e51cfcf1
tuned;

diff -r 81a75d9a9a4e -r d6de6e81574d src/Doc/System/Interfaces.thy
--- a/src/Doc/System/Interfaces.thy	Fri Jan 25 20:33:36 2013 +0100
+++ b/src/Doc/System/Interfaces.thy	Sat Jan 26 12:45:32 2013 +0100
@@ -8,7 +8,7 @@
 
 text {* The @{tool_def jedit} tool invokes a version of
   jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented
-  with some components to provide a fully-featured Prover IDE:
+  with some plugins to provide a fully-featured Prover IDE:
 \begin{ttbox} Usage: isabelle jedit [OPTIONS]
   [FILES ...]
 
@@ -37,7 +37,8 @@
   store the result session image (see also \secref{sec:tool-build}).
   The @{verbatim "-n"} option bypasses the session build dialog.
 
-  The @{verbatim "-m"} option specifies additional print modes.
+  The @{verbatim "-m"} option specifies additional print modes for the
+  prover process.
 
   The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
   additional low-level options to the JVM or jEdit, respectively.  The
@@ -61,14 +62,16 @@
   regular Isabelle settings environment (\secref{sec:settings}).  This
   is more convenient than starting Emacs separately, loading the Proof
   General LISP files, and then attempting to start Isabelle with
-  dynamic @{setting PATH} lookup etc.
+  dynamic @{setting PATH} lookup etc., although it might fail if a
+  different version of Proof General is already part of the Emacs
+  installation of the operating system.
 
   The actual interface script is part of the Proof General
   distribution; its usage depends on the particular version.  There
   are some options available, such as @{verbatim "-l"} for passing the
   logic image to be used by default, or @{verbatim "-m"} to tune the
-  standard print mode.  The following Isabelle settings are
-  particularly important for Proof General:
+  standard print mode of the prover process.  The following Isabelle
+  settings are particularly important for Proof General:
 
   \begin{description}
 
diff -r 81a75d9a9a4e -r d6de6e81574d src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Fri Jan 25 20:33:36 2013 +0100
+++ b/src/Doc/System/Presentation.thy	Sat Jan 26 12:45:32 2013 +0100
@@ -127,7 +127,7 @@
   need to be deleted manually.
 
   \medskip Option @{verbatim "-d"} indicates that the session shall be
-  accompanied by a formal document, with @{text dir}@{verbatim
+  accompanied by a formal document, with @{text DIR}@{verbatim
   "/document/root.tex"} as its {\LaTeX} entry point (see also
   \chref{ch:present}).
 
@@ -160,7 +160,7 @@
   \label{sec:tool-document} *}
 
 text {* The @{tool_def document} tool prepares logic session
-  documents, processing the sources both as provided by the user and
+  documents, processing the sources as provided by the user and
   generated by Isabelle.  Its usage is:
 \begin{ttbox}
 Usage: isabelle document [OPTIONS] [DIR]
@@ -220,9 +220,9 @@
   arguments for the document format and the document variant name.
   The script needs to produce corresponding output files, e.g.\
   @{verbatim root.pdf} for target format @{verbatim pdf} (and default
-  default variants).  The main work can be again delegated to @{tool
-  latex}, but it is also possible to harvest generated {\LaTeX}
-  sources and copy them elsewhere, for example.
+  variants).  The main work can be again delegated to @{tool latex},
+  but it is also possible to harvest generated {\LaTeX} sources and
+  copy them elsewhere.
 
   \medskip When running the session, Isabelle copies the content of
   the original @{verbatim document} directory into its proper place
@@ -249,7 +249,7 @@
   complete list of predefined Isabelle symbols.  Users may invent
   further symbols as well, just by providing {\LaTeX} macros in a
   similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of
-  the distribution.
+  the Isabelle distribution.
 
   For proper setup of DVI and PDF documents (with hyperlinks and
   bookmarks), we recommend to include @{file