1.1 --- a/src/Doc/System/Interfaces.thy	Fri Jan 25 20:33:36 2013 +0100
     1.2 +++ b/src/Doc/System/Interfaces.thy	Sat Jan 26 12:45:32 2013 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  text {* The @{tool_def jedit} tool invokes a version of
     1.6    jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented
     1.7 -  with some components to provide a fully-featured Prover IDE:
     1.8 +  with some plugins to provide a fully-featured Prover IDE:
     1.9  \begin{ttbox} Usage: isabelle jedit [OPTIONS]
    1.10    [FILES ...]
    1.11  
    1.12 @@ -37,7 +37,8 @@
    1.13    store the result session image (see also \secref{sec:tool-build}).
    1.14    The @{verbatim "-n"} option bypasses the session build dialog.
    1.15  
    1.16 -  The @{verbatim "-m"} option specifies additional print modes.
    1.17 +  The @{verbatim "-m"} option specifies additional print modes for the
    1.18 +  prover process.
    1.19  
    1.20    The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
    1.21    additional low-level options to the JVM or jEdit, respectively.  The
    1.22 @@ -61,14 +62,16 @@
    1.23    regular Isabelle settings environment (\secref{sec:settings}).  This
    1.24    is more convenient than starting Emacs separately, loading the Proof
    1.25    General LISP files, and then attempting to start Isabelle with
    1.26 -  dynamic @{setting PATH} lookup etc.
    1.27 +  dynamic @{setting PATH} lookup etc., although it might fail if a
    1.28 +  different version of Proof General is already part of the Emacs
    1.29 +  installation of the operating system.
    1.30  
    1.31    The actual interface script is part of the Proof General
    1.32    distribution; its usage depends on the particular version.  There
    1.33    are some options available, such as @{verbatim "-l"} for passing the
    1.34    logic image to be used by default, or @{verbatim "-m"} to tune the
    1.35 -  standard print mode.  The following Isabelle settings are
    1.36 -  particularly important for Proof General:
    1.37 +  standard print mode of the prover process.  The following Isabelle
    1.38 +  settings are particularly important for Proof General:
    1.39  
    1.40    \begin{description}
    1.41  

     2.1 --- a/src/Doc/System/Presentation.thy	Fri Jan 25 20:33:36 2013 +0100
     2.2 +++ b/src/Doc/System/Presentation.thy	Sat Jan 26 12:45:32 2013 +0100
     2.3 @@ -127,7 +127,7 @@
     2.4    need to be deleted manually.
     2.5  
     2.6    \medskip Option @{verbatim "-d"} indicates that the session shall be
     2.7 -  accompanied by a formal document, with @{text dir}@{verbatim
     2.8 +  accompanied by a formal document, with @{text DIR}@{verbatim
     2.9    "/document/root.tex"} as its {\LaTeX} entry point (see also
    2.10    \chref{ch:present}).
    2.11  
    2.12 @@ -160,7 +160,7 @@
    2.13    \label{sec:tool-document} *}
    2.14  
    2.15  text {* The @{tool_def document} tool prepares logic session
    2.16 -  documents, processing the sources both as provided by the user and
    2.17 +  documents, processing the sources as provided by the user and
    2.18    generated by Isabelle.  Its usage is:
    2.19  \begin{ttbox}
    2.20  Usage: isabelle document [OPTIONS] [DIR]
    2.21 @@ -220,9 +220,9 @@
    2.22    arguments for the document format and the document variant name.
    2.23    The script needs to produce corresponding output files, e.g.\
    2.24    @{verbatim root.pdf} for target format @{verbatim pdf} (and default
    2.25 -  default variants).  The main work can be again delegated to @{tool
    2.26 -  latex}, but it is also possible to harvest generated {\LaTeX}
    2.27 -  sources and copy them elsewhere, for example.
    2.28 +  variants).  The main work can be again delegated to @{tool latex},
    2.29 +  but it is also possible to harvest generated {\LaTeX} sources and
    2.30 +  copy them elsewhere.
    2.31  
    2.32    \medskip When running the session, Isabelle copies the content of
    2.33    the original @{verbatim document} directory into its proper place
    2.34 @@ -249,7 +249,7 @@
    2.35    complete list of predefined Isabelle symbols.  Users may invent
    2.36    further symbols as well, just by providing {\LaTeX} macros in a
    2.37    similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of
    2.38 -  the distribution.
    2.39 +  the Isabelle distribution.
    2.40  
    2.41    For proper setup of DVI and PDF documents (with hyperlinks and
    2.42    bookmarks), we recommend to include @{file