doc-src/System/Thy/Presentation.thy
changeset 28238 398bf960d3d4
parent 28225 5d1fc22bccdf
child 28504 7ad7d7d6df47
     1.1 --- a/doc-src/System/Thy/Presentation.thy	Tue Sep 16 14:39:56 2008 +0200
     1.2 +++ b/doc-src/System/Thy/Presentation.thy	Tue Sep 16 14:40:30 2008 +0200
     1.3 @@ -28,24 +28,25 @@
     1.4    \begin{center}
     1.5    \begin{tabular}{lp{0.6\textwidth}}
     1.6  
     1.7 -      @{verbatim "isatool mkdir"} & invoked once by the user to create
     1.8 -      the initial source setup (common @{verbatim IsaMakefile} plus a
     1.9 -      single session directory); \\
    1.10 +      @{verbatim isatool} @{tool_ref mkdir} & invoked once by the user
    1.11 +      to create the initial source setup (common @{verbatim
    1.12 +      IsaMakefile} plus a single session directory); \\
    1.13  
    1.14 -      @{verbatim "isatool make"} & invoked repeatedly by the user to
    1.15 -      keep session output up-to-date (HTML, documents etc.); \\
    1.16 +      @{verbatim isatool} @{tool make} & invoked repeatedly by the
    1.17 +      user to keep session output up-to-date (HTML, documents etc.); \\
    1.18 +
    1.19 +      @{verbatim isatool} @{tool usedir} & part of the standard
    1.20 +      @{verbatim IsaMakefile} entry of a session; \\
    1.21  
    1.22 -      @{verbatim "isatool usedir"} & part of the standard @{verbatim
    1.23 -      IsaMakefile} entry of a session; \\
    1.24 -
    1.25 -      @{verbatim "isabelle-process"} & run through @{verbatim "isatool usedir"}; \\
    1.26 +      @{executable "isabelle-process"} & run through @{verbatim
    1.27 +      isatool} @{tool_ref usedir}; \\
    1.28  
    1.29 -      @{verbatim "isatool document"} & run by the Isabelle process if
    1.30 -      document preparation is enabled; \\
    1.31 +      @{verbatim isatool} @{tool_ref document} & run by the Isabelle
    1.32 +      process if document preparation is enabled; \\
    1.33  
    1.34 -      @{verbatim "isatool latex"} & universal {\LaTeX} tool wrapper
    1.35 -      invoked multiple times by @{verbatim "isatool document"}; also
    1.36 -      useful for manual experiments; \\
    1.37 +      @{verbatim isatool} @{tool_ref latex} & universal {\LaTeX} tool
    1.38 +      wrapper invoked multiple times by @{verbatim isatool} @{tool_ref
    1.39 +      document}; also useful for manual experiments; \\
    1.40  
    1.41    \end{tabular}
    1.42    \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
    1.43 @@ -81,23 +82,23 @@
    1.44    The easiest way to let Isabelle generate theory browsing information
    1.45    for existing sessions is to append ``@{verbatim "-i true"}'' to the
    1.46    @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim
    1.47 -  "isatool make"} (or @{verbatim "./build"} in the distribution).  For
    1.48 +  isatool} @{tool make} (or @{"file" "$ISABELLE_HOME/build"}).  For
    1.49    example, add something like this to your Isabelle settings file
    1.50  
    1.51  \begin{ttbox}
    1.52  ISABELLE_USEDIR_OPTIONS="-i true"
    1.53  \end{ttbox}
    1.54  
    1.55 -  and then change into the @{verbatim "src/FOL"} directory of the
    1.56 -  Isabelle distribution and run @{verbatim "isatool make"}, or even
    1.57 -  @{verbatim "isatool make all"}.  The presentation output will appear
    1.58 -  in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
    1.59 +  and then change into the @{"file" "~~/src/FOL"} directory and run
    1.60 +  @{verbatim isatool} @{tool make}, or even @{verbatim isatool} @{tool
    1.61 +  make}~@{verbatim all}.  The presentation output will appear in
    1.62 +  @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
    1.63    @{verbatim "~/isabelle/browser_info/FOL"}.  Note that option
    1.64    @{verbatim "-v true"} will make the internal runs of @{tool usedir}
    1.65    more explicit about such details.
    1.66  
    1.67 -  Many standard Isabelle sessions (such as @{verbatim "HOL/ex"}) also
    1.68 -  provide actual printable documents.  These are prepared
    1.69 +  Many standard Isabelle sessions (such as @{"file" "~~/src/HOL/ex"})
    1.70 +  also provide actual printable documents.  These are prepared
    1.71    automatically as well if enabled like this, using the @{verbatim
    1.72    "-d"} option
    1.73  \begin{ttbox}
    1.74 @@ -134,7 +135,7 @@
    1.75  
    1.76    This assumes that directory @{verbatim Foo} contains some @{verbatim
    1.77    ROOT.ML} file to load all your theories, and HOL is your parent
    1.78 -  logic image (@{verbatim isatool}~@{tool_ref mkdir} assists in
    1.79 +  logic image (@{verbatim isatool} @{tool_ref mkdir} assists in
    1.80    setting up Isabelle session directories.  Theory browser information
    1.81    for HOL should have been generated already beforehand.
    1.82    Alternatively, one may specify an external link to an existing body
    1.83 @@ -168,7 +169,7 @@
    1.84    hidden, thus enabling the user to collapse irrelevant portions of
    1.85    information.  The browser is written in Java, it can be used both as
    1.86    a stand-alone application and as an applet.  Note that the option
    1.87 -  @{verbatim "-g"} of @{verbatim isatool}~@{tool_ref usedir} creates
    1.88 +  @{verbatim "-g"} of @{verbatim isatool} @{tool_ref usedir} creates
    1.89    graph presentations in batch mode for inclusion in session
    1.90    documents.
    1.91  *}
    1.92 @@ -341,7 +342,8 @@
    1.93    directory with a minimal @{verbatim root.tex} that is sufficient to
    1.94    print all theories of the session (in the order of appearance); see
    1.95    \secref{sec:tool-document} for further information on Isabelle
    1.96 -  document preparation.  The usage of @{verbatim "isatool mkdir"} is:
    1.97 +  document preparation.  The usage of @{verbatim isatool} @{tool
    1.98 +  mkdir} is:
    1.99  
   1.100  \begin{ttbox}
   1.101  Usage: mkdir [OPTIONS] [LOGIC] NAME
   1.102 @@ -409,8 +411,8 @@
   1.103  
   1.104    \noindent The theory sources should be put into the @{verbatim Foo}
   1.105    directory, and its @{verbatim ROOT.ML} should be edited to load all
   1.106 -  required theories.  Invoking @{verbatim "isatool make"} again would
   1.107 -  run the whole session, generating browser information and the
   1.108 +  required theories.  Invoking @{verbatim isatool} @{tool make} again
   1.109 +  would run the whole session, generating browser information and the
   1.110    document automatically.  The @{verbatim IsaMakefile} is typically
   1.111    tuned manually later, e.g.\ adding source dependencies, or changing
   1.112    the options passed to @{tool usedir}.
   1.113 @@ -420,9 +422,9 @@
   1.114    manual editing of the generated @{verbatim IsaMakefile}, which is
   1.115    meant to cover all of the sub-session directories at the same time
   1.116    (this is the deeper reasong why @{verbatim IsaMakefile} is not made
   1.117 -  part of the initial session directory created by
   1.118 -  @{verbatim "isatool mkdir"}).  See @{verbatim "src/HOL/IsaMakefile"}
   1.119 -  of the Isabelle distribution for a full-blown example.
   1.120 +  part of the initial session directory created by @{verbatim
   1.121 +  isatool} @{tool mkdir}).  See @{"file" "~~/src/HOL/IsaMakefile"} for
   1.122 +  a full-blown example.
   1.123  *}
   1.124  
   1.125  
   1.126 @@ -464,7 +466,7 @@
   1.127    Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
   1.128    setting is implicitly prefixed to \emph{any} @{tool usedir}
   1.129    call. Since the @{verbatim IsaMakefile}s of all object-logics
   1.130 -  distributed with Isabelle just invoke \texttt{usedir} for the real
   1.131 +  distributed with Isabelle just invoke @{tool usedir} for the real
   1.132    work, one may control compilation options globally via above
   1.133    variable. In particular, generation of \rmindex{HTML} browsing
   1.134    information and document preparation is controlled here.
   1.135 @@ -490,7 +492,7 @@
   1.136    directory and then quitting.  It is assumed that @{verbatim ROOT.ML}
   1.137    contains all ML commands required to build the logic.
   1.138  
   1.139 -  In example mode, @{verbatim usedir} runs a read-only session of
   1.140 +  In example mode, @{tool usedir} runs a read-only session of
   1.141    @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from
   1.142    within directory @{verbatim NAME}.  It assumes that this file
   1.143    contains appropriate ML commands to run the desired examples.
   1.144 @@ -544,13 +546,13 @@
   1.145    relative to the session's main directory.  If the @{verbatim "-C"}
   1.146    option is true, this will include a copy of an existing @{verbatim
   1.147    document} directory as provided by the user.  For example,
   1.148 -  @{verbatim "isatool usedir -D generated HOL Foo"} produces a
   1.149 -  complete set of document sources at @{verbatim "Foo/generated"}.
   1.150 -  Subsequent invocation of @{verbatim "isatool document
   1.151 -  Foo/generated"} (see also \secref{sec:tool-document}) will process
   1.152 -  the final result independently of an Isabelle job.  This decoupled
   1.153 -  mode of operation facilitates debugging of serious {\LaTeX} errors,
   1.154 -  for example.
   1.155 +  @{verbatim isatool} @{tool usedir}~@{verbatim "-D generated HOL
   1.156 +  Foo"} produces a complete set of document sources at @{verbatim
   1.157 +  "Foo/generated"}.  Subsequent invocation of @{verbatim
   1.158 +  isatool} @{tool document}~@{verbatim "Foo/generated"} (see also
   1.159 +  \secref{sec:tool-document}) will process the final result
   1.160 +  independently of an Isabelle job.  This decoupled mode of operation
   1.161 +  facilitates debugging of serious {\LaTeX} errors, for example.
   1.162  
   1.163    \medskip The @{verbatim "-p"} option determines the level of detail
   1.164    for internal proof objects, see also the \emph{Isabelle Reference
   1.165 @@ -563,14 +565,14 @@
   1.166    \medskip The @{verbatim "-M"} option specifies the maximum number of
   1.167    parallel threads used for processing independent tasks when checking
   1.168    theory sources (multithreading only works on suitable ML platforms).
   1.169 -  The special value of ``@{verbatim 0}'' or ``@{verbatim max}'' refers
   1.170 -  to the number of actual CPU cores of the underlying machine, which
   1.171 -  is a good starting point for optimal performance tuning.  The
   1.172 -  @{verbatim "-T"} option determines the level of detail in tracing
   1.173 -  output concerning the internal locking and scheduling in
   1.174 -  multithreaded operation.  This may be helpful in isolating
   1.175 -  performance bottle-necks, e.g.\ due to excessive wait states when
   1.176 -  locking critical code sections.
   1.177 +  The special value of @{verbatim 0} or @{verbatim max} refers to the
   1.178 +  number of actual CPU cores of the underlying machine, which is a
   1.179 +  good starting point for optimal performance tuning.  The @{verbatim
   1.180 +  "-T"} option determines the level of detail in tracing output
   1.181 +  concerning the internal locking and scheduling in multithreaded
   1.182 +  operation.  This may be helpful in isolating performance
   1.183 +  bottle-necks, e.g.\ due to excessive wait states when locking
   1.184 +  critical code sections.
   1.185  
   1.186    \medskip Any @{tool usedir} session is named by some \emph{session
   1.187    identifier}. These accumulate, documenting the way sessions depend
   1.188 @@ -589,7 +591,7 @@
   1.189  text {*
   1.190    Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's
   1.191    object-logics as a model for your own developments.  For example,
   1.192 -  see @{verbatim "src/FOL/IsaMakefile"}.  The Isabelle @{tool_ref
   1.193 +  see @{"file" "~~/src/FOL/IsaMakefile"}.  The Isabelle @{tool_ref
   1.194    mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation
   1.195    of @{tool usedir} as well.
   1.196  *}
   1.197 @@ -641,7 +643,8 @@
   1.198    to the tag specification ``@{verbatim
   1.199    "/theory,/proof,/ML,+visible,-invisible"}''; see also the {\LaTeX}
   1.200    macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and
   1.201 -  @{verbatim "\\isafoldtag"}, in @{verbatim isabelle.sty}.
   1.202 +  @{verbatim "\\isafoldtag"}, in @{"file"
   1.203 +  "~~/lib/texinputs/isabelle.sty"}.
   1.204  
   1.205    \medskip Document preparation requires a properly setup ``@{verbatim
   1.206    document}'' directory within the logic session sources.  This
   1.207 @@ -664,7 +667,7 @@
   1.208  
   1.209    \medskip When running the session, Isabelle copies the original
   1.210    @{verbatim document} directory into its proper place within
   1.211 -  @{verbatim ISABELLE_BROWSER_INFO} according to the session path.
   1.212 +  @{setting ISABELLE_BROWSER_INFO} according to the session path.
   1.213    Then, for any processed theory @{text A} some {\LaTeX} source is
   1.214    generated and put there as @{text A}@{verbatim ".tex"}.
   1.215    Furthermore, a list of all generated theory files is put into
   1.216 @@ -673,36 +676,36 @@
   1.217    containing all the theories.
   1.218  
   1.219    The {\LaTeX} versions of the theories require some macros defined in
   1.220 -  @{verbatim isabelle.sty} as distributed with Isabelle.  Doing
   1.221 -  @{verbatim "\\usepackage{isabelle}"} in @{verbatim root.tex} should
   1.222 -  be fine; the underlying Isabelle @{tool latex} tool already includes
   1.223 -  an appropriate path specification for {\TeX} inputs.
   1.224 +  @{"file" "~~/lib/texinputs/isabelle.sty"}.  Doing @{verbatim
   1.225 +  "\\usepackage{isabelle}"} in @{verbatim root.tex} should be fine;
   1.226 +  the underlying Isabelle @{tool latex} tool already includes an
   1.227 +  appropriate path specification for {\TeX} inputs.
   1.228  
   1.229    If the text contains any references to Isabelle symbols (such as
   1.230    @{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim
   1.231 -  isabellesym.sty} should be included as well.  This package contains
   1.232 -  a standard set of {\LaTeX} macro definitions @{verbatim
   1.233 +  "isabellesym.sty"} should be included as well.  This package
   1.234 +  contains a standard set of {\LaTeX} macro definitions @{verbatim
   1.235    "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim
   1.236    "<"}@{text foo}@{verbatim ">"}, (see \appref{app:symbols} for a
   1.237    complete list of predefined Isabelle symbols).  Users may invent
   1.238    further symbols as well, just by providing {\LaTeX} macros in a
   1.239 -  similar fashion as in @{verbatim isabellesym.sty} of the
   1.240 -  distribution.
   1.241 +  similar fashion as in @{"file" "~~/lib/texinputs/isabellesym.sty"} of
   1.242 +  the distribution.
   1.243  
   1.244    For proper setup of DVI and PDF documents (with hyperlinks and
   1.245 -  bookmarks), we recommend to include @{verbatim pdfsetup.sty} as
   1.246 -  well.
   1.247 +  bookmarks), we recommend to include @{"file"
   1.248 +  "~~/lib/texinputs/pdfsetup.sty"} as well.
   1.249  
   1.250    \medskip As a final step of document preparation within Isabelle,
   1.251 -  @{verbatim "isatool document -c"} is run on the resulting @{verbatim
   1.252 -  document} directory.  Thus the actual output document is built and
   1.253 -  installed in its proper place (as linked by the session's @{verbatim
   1.254 -  index.html} if option @{verbatim "-i"} of @{tool_ref usedir} has
   1.255 -  been enabled, cf.\ \secref{sec:info}).  The generated sources are
   1.256 -  deleted after successful run of {\LaTeX} and friends.  Note that a
   1.257 -  separate copy of the sources may be retained by passing an option
   1.258 -  @{verbatim "-D"} to the @{tool usedir} utility when running the
   1.259 -  session.
   1.260 +  @{verbatim isatool} @{tool document}~@{verbatim "-c"} is run on the
   1.261 +  resulting @{verbatim document} directory.  Thus the actual output
   1.262 +  document is built and installed in its proper place (as linked by
   1.263 +  the session's @{verbatim index.html} if option @{verbatim "-i"} of
   1.264 +  @{tool_ref usedir} has been enabled, cf.\ \secref{sec:info}).  The
   1.265 +  generated sources are deleted after successful run of {\LaTeX} and
   1.266 +  friends.  Note that a separate copy of the sources may be retained
   1.267 +  by passing an option @{verbatim "-D"} to the @{tool usedir} utility
   1.268 +  when running the session.
   1.269  *}
   1.270  
   1.271  
   1.272 @@ -745,10 +748,10 @@
   1.273  subsubsection {* Examples *}
   1.274  
   1.275  text {*
   1.276 -  Invoking @{verbatim "isatool latex"} by hand may be occasionally
   1.277 -  useful when debugging failed attempts of the automatic document
   1.278 -  preparation stage of batch-mode Isabelle.  The abortive process
   1.279 -  leaves the sources at a certain place within @{setting
   1.280 +  Invoking @{verbatim isatool} @{tool latex} by hand may be
   1.281 +  occasionally useful when debugging failed attempts of the automatic
   1.282 +  document preparation stage of batch-mode Isabelle.  The abortive
   1.283 +  process leaves the sources at a certain place within @{setting
   1.284    ISABELLE_BROWSER_INFO}, see the runtime error message for details.
   1.285    This enables users to inspect {\LaTeX} runs in further detail, e.g.\
   1.286    like this: