--- 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}
--- 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