
diff -r f1fc11c73569 -r 398bf960d3d4 doc-src/System/Thy/Presentation.thy
--- a/doc-src/System/Thy/Presentation.thy	Tue Sep 16 14:39:56 2008 +0200
+++ b/doc-src/System/Thy/Presentation.thy	Tue Sep 16 14:40:30 2008 +0200
@@ -28,24 +28,25 @@
   \begin{center}
   \begin{tabular}{lp{0.6\textwidth}}
 
-      @{verbatim "isatool mkdir"} & invoked once by the user to create
-      the initial source setup (common @{verbatim IsaMakefile} plus a
-      single session directory); \\
+      @{verbatim isatool} @{tool_ref mkdir} & invoked once by the user
+      to create the initial source setup (common @{verbatim
+      IsaMakefile} plus a single session directory); \\
 
-      @{verbatim "isatool make"} & invoked repeatedly by the user to
-      keep session output up-to-date (HTML, documents etc.); \\
+      @{verbatim isatool} @{tool make} & invoked repeatedly by the
+      user to keep session output up-to-date (HTML, documents etc.); \\
+
+      @{verbatim isatool} @{tool usedir} & part of the standard
+      @{verbatim IsaMakefile} entry of a session; \\
 
-      @{verbatim "isatool usedir"} & part of the standard @{verbatim
-      IsaMakefile} entry of a session; \\
-
-      @{verbatim "isabelle-process"} & run through @{verbatim "isatool usedir"}; \\
+      @{executable "isabelle-process"} & run through @{verbatim
+      isatool} @{tool_ref usedir}; \\
 
-      @{verbatim "isatool document"} & run by the Isabelle process if
-      document preparation is enabled; \\
+      @{verbatim isatool} @{tool_ref document} & run by the Isabelle
+      process if document preparation is enabled; \\
 
-      @{verbatim "isatool latex"} & universal {\LaTeX} tool wrapper
-      invoked multiple times by @{verbatim "isatool document"}; also
-      useful for manual experiments; \\
+      @{verbatim isatool} @{tool_ref latex} & universal {\LaTeX} tool
+      wrapper invoked multiple times by @{verbatim isatool} @{tool_ref
+      document}; also useful for manual experiments; \\
 
   \end{tabular}
   \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
@@ -81,23 +82,23 @@
   The easiest way to let Isabelle generate theory browsing information
   for existing sessions is to append ``@{verbatim "-i true"}'' to the
   @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim
-  "isatool make"} (or @{verbatim "./build"} in the distribution).  For
+  isatool} @{tool make} (or @{"file" "$ISABELLE_HOME/build"}).  For
   example, add something like this to your Isabelle settings file
 
 \begin{ttbox}
 ISABELLE_USEDIR_OPTIONS="-i true"
 \end{ttbox}
 
-  and then change into the @{verbatim "src/FOL"} directory of the
-  Isabelle distribution and run @{verbatim "isatool make"}, or even
-  @{verbatim "isatool make all"}.  The presentation output will appear
-  in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
+  and then change into the @{"file" "~~/src/FOL"} directory and run
+  @{verbatim isatool} @{tool make}, or even @{verbatim isatool} @{tool
+  make}~@{verbatim all}.  The presentation output will appear in
+  @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
   @{verbatim "~/isabelle/browser_info/FOL"}.  Note that option
   @{verbatim "-v true"} will make the internal runs of @{tool usedir}
   more explicit about such details.
 
-  Many standard Isabelle sessions (such as @{verbatim "HOL/ex"}) also
-  provide actual printable documents.  These are prepared
+  Many standard Isabelle sessions (such as @{"file" "~~/src/HOL/ex"})
+  also provide actual printable documents.  These are prepared
   automatically as well if enabled like this, using the @{verbatim
   "-d"} option
 \begin{ttbox}
@@ -134,7 +135,7 @@
 
   This assumes that directory @{verbatim Foo} contains some @{verbatim
   ROOT.ML} file to load all your theories, and HOL is your parent
-  logic image (@{verbatim isatool}~@{tool_ref mkdir} assists in
+  logic image (@{verbatim isatool} @{tool_ref mkdir} assists in
   setting up Isabelle session directories.  Theory browser information
   for HOL should have been generated already beforehand.
   Alternatively, one may specify an external link to an existing body
@@ -168,7 +169,7 @@
   hidden, thus enabling the user to collapse irrelevant portions of
   information.  The browser is written in Java, it can be used both as
   a stand-alone application and as an applet.  Note that the option
-  @{verbatim "-g"} of @{verbatim isatool}~@{tool_ref usedir} creates
+  @{verbatim "-g"} of @{verbatim isatool} @{tool_ref usedir} creates
   graph presentations in batch mode for inclusion in session
   documents.
 *}
@@ -341,7 +342,8 @@
   directory with a minimal @{verbatim root.tex} that is sufficient to
   print all theories of the session (in the order of appearance); see
   \secref{sec:tool-document} for further information on Isabelle
-  document preparation.  The usage of @{verbatim "isatool mkdir"} is:
+  document preparation.  The usage of @{verbatim isatool} @{tool
+  mkdir} is:
 
 \begin{ttbox}
 Usage: mkdir [OPTIONS] [LOGIC] NAME
@@ -409,8 +411,8 @@
 
   \noindent The theory sources should be put into the @{verbatim Foo}
   directory, and its @{verbatim ROOT.ML} should be edited to load all
-  required theories.  Invoking @{verbatim "isatool make"} again would
-  run the whole session, generating browser information and the
+  required theories.  Invoking @{verbatim isatool} @{tool make} again
+  would run the whole session, generating browser information and the
   document automatically.  The @{verbatim IsaMakefile} is typically
   tuned manually later, e.g.\ adding source dependencies, or changing
   the options passed to @{tool usedir}.
@@ -420,9 +422,9 @@
   manual editing of the generated @{verbatim IsaMakefile}, which is
   meant to cover all of the sub-session directories at the same time
   (this is the deeper reasong why @{verbatim IsaMakefile} is not made
-  part of the initial session directory created by
-  @{verbatim "isatool mkdir"}).  See @{verbatim "src/HOL/IsaMakefile"}
-  of the Isabelle distribution for a full-blown example.
+  part of the initial session directory created by @{verbatim
+  isatool} @{tool mkdir}).  See @{"file" "~~/src/HOL/IsaMakefile"} for
+  a full-blown example.
 *}
 
 
@@ -464,7 +466,7 @@
   Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
   setting is implicitly prefixed to \emph{any} @{tool usedir}
   call. Since the @{verbatim IsaMakefile}s of all object-logics
-  distributed with Isabelle just invoke \texttt{usedir} for the real
+  distributed with Isabelle just invoke @{tool usedir} for the real
   work, one may control compilation options globally via above
   variable. In particular, generation of \rmindex{HTML} browsing
   information and document preparation is controlled here.
@@ -490,7 +492,7 @@
   directory and then quitting.  It is assumed that @{verbatim ROOT.ML}
   contains all ML commands required to build the logic.
 
-  In example mode, @{verbatim usedir} runs a read-only session of
+  In example mode, @{tool usedir} runs a read-only session of
   @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from
   within directory @{verbatim NAME}.  It assumes that this file
   contains appropriate ML commands to run the desired examples.
@@ -544,13 +546,13 @@
   relative to the session's main directory.  If the @{verbatim "-C"}
   option is true, this will include a copy of an existing @{verbatim
   document} directory as provided by the user.  For example,
-  @{verbatim "isatool usedir -D generated HOL Foo"} produces a
-  complete set of document sources at @{verbatim "Foo/generated"}.
-  Subsequent invocation of @{verbatim "isatool document
-  Foo/generated"} (see also \secref{sec:tool-document}) will process
-  the final result independently of an Isabelle job.  This decoupled
-  mode of operation facilitates debugging of serious {\LaTeX} errors,
-  for example.
+  @{verbatim isatool} @{tool usedir}~@{verbatim "-D generated HOL
+  Foo"} produces a complete set of document sources at @{verbatim
+  "Foo/generated"}.  Subsequent invocation of @{verbatim
+  isatool} @{tool document}~@{verbatim "Foo/generated"} (see also
+  \secref{sec:tool-document}) will process the final result
+  independently of an Isabelle job.  This decoupled mode of operation
+  facilitates debugging of serious {\LaTeX} errors, for example.
 
   \medskip The @{verbatim "-p"} option determines the level of detail
   for internal proof objects, see also the \emph{Isabelle Reference
@@ -563,14 +565,14 @@
   \medskip The @{verbatim "-M"} option specifies the maximum number of
   parallel threads used for processing independent tasks when checking
   theory sources (multithreading only works on suitable ML platforms).
-  The special value of ``@{verbatim 0}'' or ``@{verbatim max}'' refers
-  to the number of actual CPU cores of the underlying machine, which
-  is a good starting point for optimal performance tuning.  The
-  @{verbatim "-T"} option determines the level of detail in tracing
-  output concerning the internal locking and scheduling in
-  multithreaded operation.  This may be helpful in isolating
-  performance bottle-necks, e.g.\ due to excessive wait states when
-  locking critical code sections.
+  The special value of @{verbatim 0} or @{verbatim max} refers to the
+  number of actual CPU cores of the underlying machine, which is a
+  good starting point for optimal performance tuning.  The @{verbatim
+  "-T"} option determines the level of detail in tracing output
+  concerning the internal locking and scheduling in multithreaded
+  operation.  This may be helpful in isolating performance
+  bottle-necks, e.g.\ due to excessive wait states when locking
+  critical code sections.
 
   \medskip Any @{tool usedir} session is named by some \emph{session
   identifier}. These accumulate, documenting the way sessions depend
@@ -589,7 +591,7 @@
 text {*
   Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's
   object-logics as a model for your own developments.  For example,
-  see @{verbatim "src/FOL/IsaMakefile"}.  The Isabelle @{tool_ref
+  see @{"file" "~~/src/FOL/IsaMakefile"}.  The Isabelle @{tool_ref
   mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation
   of @{tool usedir} as well.
 *}
@@ -641,7 +643,8 @@
   to the tag specification ``@{verbatim
   "/theory,/proof,/ML,+visible,-invisible"}''; see also the {\LaTeX}
   macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and
-  @{verbatim "\\isafoldtag"}, in @{verbatim isabelle.sty}.
+  @{verbatim "\\isafoldtag"}, in @{"file"
+  "~~/lib/texinputs/isabelle.sty"}.
 
   \medskip Document preparation requires a properly setup ``@{verbatim
   document}'' directory within the logic session sources.  This
@@ -664,7 +667,7 @@
 
   \medskip When running the session, Isabelle copies the original
   @{verbatim document} directory into its proper place within
-  @{verbatim ISABELLE_BROWSER_INFO} according to the session path.
+  @{setting ISABELLE_BROWSER_INFO} according to the session path.
   Then, for any processed theory @{text A} some {\LaTeX} source is
   generated and put there as @{text A}@{verbatim ".tex"}.
   Furthermore, a list of all generated theory files is put into
@@ -673,36 +676,36 @@
   containing all the theories.
 
   The {\LaTeX} versions of the theories require some macros defined in
-  @{verbatim isabelle.sty} as distributed with Isabelle.  Doing
-  @{verbatim "\\usepackage{isabelle}"} in @{verbatim root.tex} should
-  be fine; the underlying Isabelle @{tool latex} tool already includes
-  an appropriate path specification for {\TeX} inputs.
+  @{"file" "~~/lib/texinputs/isabelle.sty"}.  Doing @{verbatim
+  "\\usepackage{isabelle}"} in @{verbatim root.tex} should be fine;
+  the underlying Isabelle @{tool latex} tool already includes an
+  appropriate path specification for {\TeX} inputs.
 
   If the text contains any references to Isabelle symbols (such as
   @{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim
-  isabellesym.sty} should be included as well.  This package contains
-  a standard set of {\LaTeX} macro definitions @{verbatim
+  "isabellesym.sty"} should be included as well.  This package
+  contains a standard set of {\LaTeX} macro definitions @{verbatim
   "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim
   "<"}@{text foo}@{verbatim ">"}, (see \appref{app:symbols} for a
   complete list of predefined Isabelle symbols).  Users may invent
   further symbols as well, just by providing {\LaTeX} macros in a
-  similar fashion as in @{verbatim isabellesym.sty} of the
-  distribution.
+  similar fashion as in @{"file" "~~/lib/texinputs/isabellesym.sty"} of
+  the distribution.
 
   For proper setup of DVI and PDF documents (with hyperlinks and
-  bookmarks), we recommend to include @{verbatim pdfsetup.sty} as
-  well.
+  bookmarks), we recommend to include @{"file"
+  "~~/lib/texinputs/pdfsetup.sty"} as well.
 
   \medskip As a final step of document preparation within Isabelle,
-  @{verbatim "isatool document -c"} is run on the resulting @{verbatim
-  document} directory.  Thus the actual output document is built and
-  installed in its proper place (as linked by the session's @{verbatim
-  index.html} if option @{verbatim "-i"} of @{tool_ref usedir} has
-  been enabled, cf.\ \secref{sec:info}).  The generated sources are
-  deleted after successful run of {\LaTeX} and friends.  Note that a
-  separate copy of the sources may be retained by passing an option
-  @{verbatim "-D"} to the @{tool usedir} utility when running the
-  session.
+  @{verbatim isatool} @{tool document}~@{verbatim "-c"} is run on the
+  resulting @{verbatim document} directory.  Thus the actual output
+  document is built and installed in its proper place (as linked by
+  the session's @{verbatim index.html} if option @{verbatim "-i"} of
+  @{tool_ref usedir} has been enabled, cf.\ \secref{sec:info}).  The
+  generated sources are deleted after successful run of {\LaTeX} and
+  friends.  Note that a separate copy of the sources may be retained
+  by passing an option @{verbatim "-D"} to the @{tool usedir} utility
+  when running the session.
 *}
 
 
@@ -745,10 +748,10 @@
 subsubsection {* Examples *}
 
 text {*
-  Invoking @{verbatim "isatool latex"} by hand may be occasionally
-  useful when debugging failed attempts of the automatic document
-  preparation stage of batch-mode Isabelle.  The abortive process
-  leaves the sources at a certain place within @{setting
+  Invoking @{verbatim isatool} @{tool latex} by hand may be
+  occasionally useful when debugging failed attempts of the automatic
+  document preparation stage of batch-mode Isabelle.  The abortive
+  process leaves the sources at a certain place within @{setting
   ISABELLE_BROWSER_INFO}, see the runtime error message for details.
   This enables users to inspect {\LaTeX} runs in further detail, e.g.\
   like this:




