--- a/doc-src/System/Thy/Basics.thy Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/System/Thy/Basics.thy Mon Jul 30 14:11:29 2012 +0200
@@ -80,7 +80,7 @@
You should not try to set @{setting ISABELLE_HOME} manually. Also
note that the Isabelle executables either have to be run from their
original location in the distribution directory, or via the
- executable objects created by the @{tool install} utility. Symbolic
+ executable objects created by the @{tool install} tool. Symbolic
links are admissible, but a plain copy of the @{file
"$ISABELLE_HOME/bin"} files will not work!
@@ -137,12 +137,11 @@
\end{itemize}
\medskip Note that the settings environment may be inspected with
- the Isabelle tool @{tool getenv}. This might help to figure out the
- effect of complex settings scripts.
-*}
+ the @{tool getenv} tool. This might help to figure out the effect
+ of complex settings scripts. *}
-subsection{* Common variables *}
+subsection {* Common variables *}
text {*
This is a reference of common Isabelle settings variables. Note that
@@ -246,7 +245,7 @@
\item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed
to the command line of any @{tool_ref usedir} invocation. This
typically contains compilation options for object-logics --- @{tool
- usedir} is the basic utility for managing logic sessions (cf.\ the
+ usedir} is the basic tool for managing logic sessions (cf.\ the
@{verbatim IsaMakefile}s in the distribution).
\item[@{setting_def ISABELLE_LATEX}, @{setting_def
@@ -476,7 +475,7 @@
\medskip Note that manual session management like this does
\emph{not} provide proper setup for theory presentation. This would
- require the @{tool usedir} utility.
+ require @{tool usedir}.
\bigskip The next example demonstrates batch execution of Isabelle.
We retrieve the @{verbatim Main} theory value from the theory loader
--- a/doc-src/System/Thy/Interfaces.thy Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/System/Thy/Interfaces.thy Mon Jul 30 14:11:29 2012 +0200
@@ -115,19 +115,16 @@
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 isabelle} @{tool_ref usedir} creates
- graph presentations in batch mode for inclusion in session
- documents. *}
+ @{verbatim "-g"} of @{tool_ref usedir} creates graph presentations
+ in batch mode for inclusion in session documents. *}
subsection {* Invoking the graph browser *}
-text {*
- The stand-alone version of the graph browser is wrapped up as an
- Isabelle tool called @{tool_def browser}:
-
+text {* The stand-alone version of the graph browser is wrapped up as
+ @{tool_def browser}:
\begin{ttbox}
-Usage: browser [OPTIONS] [GRAPHFILE]
+Usage: isabelle browser [OPTIONS] [GRAPHFILE]
Options are:
-b Admin/build only
--- a/doc-src/System/Thy/Misc.thy Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/System/Thy/Misc.thy Mon Jul 30 14:11:29 2012 +0200
@@ -12,11 +12,10 @@
section {* Displaying documents *}
-text {*
- The @{tool_def display} utility displays documents in DVI or PDF
+text {* The @{tool_def display} tool displays documents in DVI or PDF
format:
\begin{ttbox}
-Usage: display [OPTIONS] FILE
+Usage: isabelle display [OPTIONS] FILE
Options are:
-c cleanup -- remove FILE after use
@@ -33,9 +32,9 @@
section {* Viewing documentation \label{sec:tool-doc} *}
text {*
- The @{tool_def doc} utility displays online documentation:
+ The @{tool_def doc} tool displays online documentation:
\begin{ttbox}
-Usage: doc [DOC]
+Usage: isabelle doc [DOC]
View Isabelle documentation DOC, or show list of available documents.
\end{ttbox}
@@ -53,10 +52,9 @@
section {* Shell commands within the settings environment \label{sec:tool-env} *}
-text {* The @{tool_def env} utility is a direct wrapper for the
- standard @{verbatim "/usr/bin/env"} command on POSIX systems,
- running within the Isabelle settings environment
- (\secref{sec:settings}).
+text {* The @{tool_def env} tool is a direct wrapper for the standard
+ @{verbatim "/usr/bin/env"} command on POSIX systems, running within
+ the Isabelle settings environment (\secref{sec:settings}).
The command-line arguments are that of the underlying version of
@{verbatim env}. For example, the following invokes an instance of
@@ -69,8 +67,7 @@
section {* Getting logic images *}
-text {*
- The @{tool_def findlogics} utility traverses all directories
+text {* The @{tool_def findlogics} tool traverses all directories
specified in @{setting ISABELLE_PATH}, looking for Isabelle logic
images. Its usage is:
\begin{ttbox}
@@ -89,12 +86,11 @@
section {* Inspecting the settings environment \label{sec:tool-getenv} *}
-text {*
- The Isabelle settings environment --- as provided by the
+text {* The Isabelle settings environment --- as provided by the
site-default and user-specific settings files --- can be inspected
- with the @{tool_def getenv} utility:
+ with the @{tool_def getenv} tool:
\begin{ttbox}
-Usage: getenv [OPTIONS] [VARNAMES ...]
+Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
Options are:
-a display complete environment
@@ -150,14 +146,13 @@
section {* Installing standalone Isabelle executables \label{sec:tool-install} *}
-text {*
- By default, the main Isabelle binaries (@{executable "isabelle"}
- etc.) are just run from their location within the distribution
- directory, probably indirectly by the shell through its @{setting
- PATH}. Other schemes of installation are supported by the
- @{tool_def install} utility:
+text {* By default, the main Isabelle binaries (@{executable
+ "isabelle"} etc.) are just run from their location within the
+ distribution directory, probably indirectly by the shell through its
+ @{setting PATH}. Other schemes of installation are supported by the
+ @{tool_def install} tool:
\begin{ttbox}
-Usage: install [OPTIONS]
+Usage: isabelle install [OPTIONS]
Options are:
-d DISTDIR use DISTDIR as Isabelle distribution
@@ -185,11 +180,10 @@
section {* Creating instances of the Isabelle logo *}
-text {*
- The @{tool_def logo} utility creates any instance of the generic
+text {* The @{tool_def logo} tool creates any instance of the generic
Isabelle logo as an Encapsuled Postscript file (EPS):
\begin{ttbox}
-Usage: logo [OPTIONS] NAME
+Usage: isabelle logo [OPTIONS] NAME
Create instance NAME of the Isabelle logo (as EPS).
@@ -198,18 +192,16 @@
-q quiet mode
\end{ttbox}
You are encouraged to use this to create a derived logo for your
- Isabelle project. For example, @{verbatim isabelle} @{tool
- logo}~@{verbatim Bali} creates @{verbatim isabelle_bali.eps}.
-*}
+ Isabelle project. For example, @{tool logo}~@{verbatim Bali}
+ creates @{verbatim isabelle_bali.eps}. *}
section {* Isabelle's version of make \label{sec:tool-make} *}
-text {*
- The Isabelle @{tool_def make} utility is a very simple wrapper for
+text {* The @{tool_def make} tool is a very simple wrapper for
ordinary Unix @{executable make}:
\begin{ttbox}
-Usage: make [ARGS ...]
+Usage: isabelle make [ARGS ...]
Compile the logic in current directory using IsaMakefile.
ARGS are directly passed to the system make program.
@@ -219,7 +211,7 @@
may refer to its values within the @{verbatim IsaMakefile}, e.g.\
@{verbatim "$(ISABELLE_OUTPUT)"}. Furthermore, programs started from
the make file also inherit this environment. Typically, @{verbatim
- IsaMakefile}s defer the real work to the @{tool_ref usedir} utility.
+ IsaMakefile}s defer the real work to @{tool_ref usedir}.
\medskip The basic @{verbatim IsaMakefile} convention is that the
default target builds the actual logic, including its parents if
@@ -241,11 +233,11 @@
section {* Make all logics *}
-text {* The @{tool_def makeall} utility applies Isabelle make to any
+text {* The @{tool_def makeall} tool applies Isabelle make to any
Isabelle component (cf.\ \secref{sec:components}) that contains an
@{verbatim IsaMakefile}:
\begin{ttbox}
-Usage: makeall [ARGS ...]
+Usage: isabelle makeall [ARGS ...]
Apply isabelle make to all components with IsaMakefile (passing ARGS).
\end{ttbox}
@@ -258,9 +250,9 @@
section {* Printing documents *}
text {*
- The @{tool_def print} utility prints documents:
+ The @{tool_def print} tool prints documents:
\begin{ttbox}
-Usage: print [OPTIONS] FILE
+Usage: isabelle print [OPTIONS] FILE
Options are:
-c cleanup -- remove FILE after use
@@ -277,13 +269,13 @@
section {* Remove awkward symbol names from theory sources *}
text {*
- The @{tool_def unsymbolize} utility tunes Isabelle theory sources to
+ The @{tool_def unsymbolize} tool tunes Isabelle theory sources to
improve readability for plain ASCII output (e.g.\ in email
communication). Most notably, @{tool unsymbolize} replaces awkward
arrow symbols such as @{verbatim "\\"}@{verbatim "<Longrightarrow>"}
by @{verbatim "==>"}.
\begin{ttbox}
-Usage: unsymbolize [FILES|DIRS...]
+Usage: isabelle unsymbolize [FILES|DIRS...]
Recursively find .thy/.ML files, removing unreadable symbol names.
Note: this is an ad-hoc script; there is no systematic way to replace
@@ -297,7 +289,7 @@
section {* Output the version identifier of the Isabelle distribution *}
text {*
- The @{tool_def version} utility displays Isabelle version information:
+ The @{tool_def version} tool displays Isabelle version information:
\begin{ttbox}
Usage: isabelle version [OPTIONS]
--- a/doc-src/System/Thy/Presentation.thy Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/System/Thy/Presentation.thy Mon Jul 30 14:11:29 2012 +0200
@@ -13,38 +13,38 @@
(e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions
in leaf positions (usually without a separate image).
- The Isabelle tools @{tool_ref mkdir} and @{tool_ref make} provide
- the primary means for managing Isabelle sessions, including proper
- setup for presentation. Here the @{tool_ref usedir} tool takes care
- to let @{executable_ref "isabelle-process"} process run any
- additional stages required for document preparation, notably the
- tools @{tool_ref document} and @{tool_ref latex}. The complete tool
- chain for managing batch-mode Isabelle sessions is illustrated in
+ The tools @{tool_ref mkdir} and @{tool_ref make} provide the primary
+ means for managing Isabelle sessions, including proper setup for
+ presentation. Here @{tool_ref usedir} takes care to let
+ @{executable_ref "isabelle-process"} process run any additional
+ stages required for document preparation, notably the tools
+ @{tool_ref document} and @{tool_ref latex}. The complete tool chain
+ for managing batch-mode Isabelle sessions is illustrated in
\figref{fig:session-tools}.
\begin{figure}[htbp]
\begin{center}
\begin{tabular}{lp{0.6\textwidth}}
- @{verbatim isabelle} @{tool_ref mkdir} & invoked once by the user
- to create the initial source setup (common @{verbatim
- IsaMakefile} plus a single session directory); \\
+ @{tool_ref mkdir} & invoked once by the user to create the
+ initial source setup (common @{verbatim IsaMakefile} plus a
+ single session directory); \\
- @{verbatim isabelle} @{tool make} & invoked repeatedly by the
- user to keep session output up-to-date (HTML, documents etc.); \\
+ @{tool make} & invoked repeatedly by the user to keep session
+ output up-to-date (HTML, documents etc.); \\
- @{verbatim isabelle} @{tool usedir} & part of the standard
- @{verbatim IsaMakefile} entry of a session; \\
+ @{tool usedir} & part of the standard @{verbatim IsaMakefile}
+ entry of a session; \\
- @{executable "isabelle-process"} & run through @{verbatim
- isabelle} @{tool_ref usedir}; \\
+ @{executable "isabelle-process"} & run through @{tool_ref
+ usedir}; \\
- @{verbatim isabelle} @{tool_ref document} & run by the Isabelle
- process if document preparation is enabled; \\
+ @{tool_ref document} & run by the Isabelle process if document
+ preparation is enabled; \\
- @{verbatim isabelle} @{tool_ref latex} & universal {\LaTeX} tool
- wrapper invoked multiple times by @{verbatim isabelle} @{tool_ref
- document}; also useful for manual experiments; \\
+ @{tool_ref latex} & universal {\LaTeX} tool wrapper invoked
+ multiple times by @{tool_ref document}; also useful for manual
+ experiments; \\
\end{tabular}
\caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
@@ -79,22 +79,20 @@
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
- isabelle} @{tool make}. For example, add something like this to
- your Isabelle settings file
+ @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{tool make}.
+ 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 @{file "~~/src/FOL"} directory and run
- @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle}
- @{tool make}~@{verbatim all}. The presentation output will appear
- in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
- something like @{verbatim
- "~/.isabelle/IsabelleXXXX/browser_info/FOL"}. Note that option
- @{verbatim "-v true"} will make the internal runs of @{tool usedir}
- more explicit about such details.
+ @{tool make}, or even @{tool make}~@{verbatim all}. The
+ presentation output will appear in @{verbatim
+ "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to something like
+ @{verbatim "~/.isabelle/IsabelleXXXX/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 @{file "~~/src/HOL/ex"})
also provide actual printable documents. These are prepared
@@ -134,21 +132,19 @@
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 isabelle} @{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
- of HTML data by giving @{tool usedir} a @{verbatim "-P"} option like
- this:
+ logic image (@{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 of HTML data by giving @{tool
+ usedir} a @{verbatim "-P"} option like this:
\begin{ttbox}
isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
\end{ttbox}
- \medskip For production use, the @{tool usedir} tool is usually
- invoked in an appropriate @{verbatim IsaMakefile}, via the Isabelle
- @{tool make} tool. There is a separate @{tool mkdir} tool to
- provide easy setup of all this, with only minimal manual editing
- required.
+ \medskip For production use, @{tool usedir} is usually invoked in an
+ appropriate @{verbatim IsaMakefile}, via @{tool make}. There is a
+ separate @{tool mkdir} tool to provide easy setup of all this, with
+ only minimal manual editing required.
\begin{ttbox}
isabelle mkdir HOL Foo && isabelle make
\end{ttbox}
@@ -160,18 +156,16 @@
section {* Creating Isabelle session directories
\label{sec:tool-mkdir} *}
-text {*
- The @{tool_def mkdir} utility prepares Isabelle session source
+text {* The @{tool_def mkdir} tool prepares Isabelle session source
directories, including a sensible default setup of @{verbatim
IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document}
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 isabelle} @{tool
- mkdir} is:
+ document preparation. The usage of @{tool mkdir} is:
\begin{ttbox}
-Usage: mkdir [OPTIONS] [LOGIC] NAME
+Usage: isabelle mkdir [OPTIONS] [LOGIC] NAME
Options are:
-I FILE alternative IsaMakefile output
@@ -217,7 +211,7 @@
@{verbatim IsaMakefile} would be placed into a separate directory
@{verbatim NAME}, rather than the current one. See
\secref{sec:tool-usedir} for further information on \emph{build
- mode} vs.\ \emph{example mode} of the @{tool usedir} utility.
+ mode} vs.\ \emph{example mode} of @{tool usedir}.
\medskip The @{verbatim "-q"} option enables quiet mode, suppressing
further notes on how to proceed.
@@ -236,30 +230,27 @@
\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 isabelle} @{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}.
+ required theories. Invoking @{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}.
\medskip Large projects may demand further sessions, potentially
with separate logic images being created. This usually requires
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
- isabelle} @{tool mkdir}). See @{file "~~/src/HOL/IsaMakefile"} for
- a full-blown example.
-*}
+ part of the initial session directory created by @{tool mkdir}).
+ See @{file "~~/src/HOL/IsaMakefile"} for a full-blown example. *}
section {* Running Isabelle sessions \label{sec:tool-usedir} *}
-text {*
- The @{tool_def usedir} utility builds object-logic images, or runs
- example sessions based on existing logics. Its usage is:
+text {* The @{tool_def usedir} tool builds object-logic images, or
+ runs example sessions based on existing logics. Its usage is:
\begin{ttbox}
-Usage: usedir [OPTIONS] LOGIC NAME
+Usage: isabelle usedir [OPTIONS] LOGIC NAME
Options are:
-C BOOL copy existing document directory to -D PATH (default true)
@@ -344,8 +335,8 @@
\medskip The @{verbatim "-V"} option declares alternative document
variants, consisting of name/tags pairs (cf.\ options @{verbatim
- "-n"} and @{verbatim "-t"} of the @{tool_ref document} tool). The
- standard document is equivalent to ``@{verbatim
+ "-n"} and @{verbatim "-t"} of @{tool_ref document}). The standard
+ document is equivalent to ``@{verbatim
"document=theory,proof,ML"}'', which means that all theory begin/end
commands, proof body texts, and ML code will be presented
faithfully. An alternative variant ``@{verbatim
@@ -370,11 +361,10 @@
sources to be dumped at location @{verbatim PATH}; this path is
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 isabelle} @{tool usedir}~@{verbatim "-D generated HOL
- Foo"} produces a complete set of document sources at @{verbatim
- "Foo/generated"}. Subsequent invocation of @{verbatim
- isabelle} @{tool document}~@{verbatim "Foo/generated"} (see also
+ document} directory as provided by the user. For example, @{tool
+ usedir}~@{verbatim "-D generated HOL Foo"} produces a complete set
+ of document sources at @{verbatim "Foo/generated"}. Subsequent
+ invocation of @{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.
@@ -425,24 +415,21 @@
subsubsection {* Examples *}
-text {*
- Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's
- object-logics as a model for your own developments. For example,
- see @{file "~~/src/FOL/IsaMakefile"}. The Isabelle @{tool_ref
+text {* Refer to the @{verbatim IsaMakefile}s of the Isabelle
+ distribution's object-logics as a model for your own developments.
+ For example, see @{file "~~/src/FOL/IsaMakefile"}. The @{tool_ref
mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation
- of @{tool usedir} as well.
-*}
+ of @{tool usedir} as well. *}
section {* Preparing Isabelle session documents
\label{sec:tool-document} *}
-text {*
- The @{tool_def document} utility prepares logic session documents,
- processing the sources both as provided by the user and generated by
- Isabelle. Its usage is:
+text {* The @{tool_def document} tool prepares logic session
+ documents, processing the sources both as provided by the user and
+ generated by Isabelle. Its usage is:
\begin{ttbox}
-Usage: document [OPTIONS] [DIR]
+Usage: isabelle document [OPTIONS] [DIR]
Options are:
-c cleanup -- be aggressive in removing old stuff
@@ -456,13 +443,13 @@
\end{ttbox}
This tool is usually run automatically as part of the corresponding
Isabelle batch process, provided document preparation has been
- enabled (cf.\ the @{verbatim "-d"} option of the @{tool_ref usedir}
- tool). It may be manually invoked on the generated browser
- information document output as well, e.g.\ in case of errors
- encountered in the batch run.
+ enabled (cf.\ the @{verbatim "-d"} option of @{tool_ref usedir}).
+ It may be manually invoked on the generated browser information
+ document output as well, e.g.\ in case of errors encountered in the
+ batch run.
- \medskip The @{verbatim "-c"} option tells the @{tool document} tool
- to dispose the document sources after successful operation. This is
+ \medskip The @{verbatim "-c"} option tells @{tool document} to
+ dispose the document sources after successful operation. This is
the right thing to do for sources generated by an Isabelle process,
but take care of your files in manual document preparation!
@@ -489,8 +476,8 @@
final document --- apart from the actual theories which are
generated by Isabelle.
- \medskip For most practical purposes, the @{tool document} tool is
- smart enough to create any of the specified output formats, taking
+ \medskip For most practical purposes, @{tool document} is smart
+ enough to create any of the specified output formats, taking
@{verbatim root.tex} supplied by the user as a starting point. This
even includes multiple runs of {\LaTeX} to accommodate references
and bibliographies (the latter assumes @{verbatim root.bib} within
@@ -515,8 +502,8 @@
The {\LaTeX} versions of the theories require some macros defined in
@{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.
+ the underlying @{tool latex} 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
@@ -534,26 +521,23 @@
"~~/lib/texinputs/pdfsetup.sty"} as well.
\medskip As a final step of document preparation within Isabelle,
- @{verbatim isabelle} @{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.
-*}
+ @{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 @{tool usedir} when running the session. *}
section {* Running {\LaTeX} within the Isabelle environment
\label{sec:tool-latex} *}
-text {*
- The @{tool_def latex} utility provides the basic interface for
+text {* The @{tool_def latex} tool provides the basic interface for
Isabelle document preparation. Its usage is:
\begin{ttbox}
-Usage: latex [OPTIONS] [FILE]
+Usage: isabelle latex [OPTIONS] [FILE]
Options are:
-o FORMAT specify output format: dvi (default), dvi.gz, ps,
@@ -573,8 +557,8 @@
The @{verbatim sty} output format causes the Isabelle style files to
be updated from the distribution. This is useful in special
situations where the document sources are to be processed another
- time by separate tools (cf.\ option @{verbatim "-D"} of the @{tool
- usedir} utility).
+ time by separate tools (cf.\ option @{verbatim "-D"} of @{tool
+ usedir}).
The @{verbatim syms} output is for internal use; it generates lists
of symbols that are available without loading additional {\LaTeX}
@@ -584,14 +568,13 @@
subsubsection {* Examples *}
-text {*
- Invoking @{verbatim isabelle} @{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:
+text {* Invoking @{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:
+
\begin{ttbox}
cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
isabelle latex -o pdf
--- a/doc-src/System/Thy/Scala.thy Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/System/Thy/Scala.thy Mon Jul 30 14:11:29 2012 +0200
@@ -14,8 +14,8 @@
section {* Java Runtime Environment within Isabelle \label{sec:tool-java} *}
-text {* The Isabelle @{tool_def java} utility is a direct wrapper for
- the Java Runtime Environment, within the regular Isabelle settings
+text {* The @{tool_def java} tool is a direct wrapper for the Java
+ Runtime Environment, within the regular Isabelle settings
environment (\secref{sec:settings}). The command line arguments are
that of the underlying Java version. It is run in @{verbatim
"-server"} mode if possible, to improve performance (at the cost of
@@ -38,9 +38,9 @@
section {* Scala toplevel \label{sec:tool-scala} *}
-text {* The Isabelle @{tool_def scala} utility is a direct wrapper for
- the Scala toplevel; see also @{tool java} above. The command line
- arguments are that of the underlying Scala version.
+text {* The @{tool_def scala} tool is a direct wrapper for the Scala
+ toplevel; see also @{tool java} above. The command line arguments
+ are that of the underlying Scala version.
This allows to interact with Isabelle/Scala in TTY mode like this:
\begin{alltt}
@@ -53,9 +53,9 @@
section {* Scala compiler \label{sec:tool-scalac} *}
-text {* The Isabelle @{tool_def scalac} utility is a direct wrapper
- for the Scala compiler; see also @{tool scala} above. The command
- line arguments are that of the underlying Scala version.
+text {* The @{tool_def scalac} tool is a direct wrapper for the Scala
+ compiler; see also @{tool scala} above. The command line arguments
+ are that of the underlying Scala version.
This allows to compile further Scala modules, depending on existing
Isabelle/Scala functionality. The resulting class or jar files can
--- a/doc-src/System/Thy/Sessions.thy Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy Mon Jul 30 14:11:29 2012 +0200
@@ -155,14 +155,15 @@
section {* Invoking the build process \label{sec:tool-build} *}
-text {* The @{tool_def build} utility invokes the build process for
+text {* The @{tool_def build} tool invokes the build process for
Isabelle sessions. It manages dependencies between sessions,
related sources of theories and auxiliary files, and target heap
images. Accordingly, it runs instances of the prover process with
optional document preparation. Its command-line usage
is:\footnote{Isabelle/Scala provides the same functionality via
\texttt{isabelle.Build.build}.}
-\begin{ttbox} Usage: isabelle build [OPTIONS] [SESSIONS ...]
+\begin{ttbox}
+Usage: isabelle build [OPTIONS] [SESSIONS ...]
Options are:
-a select all sessions
--- a/doc-src/System/Thy/document/Basics.tex Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/System/Thy/document/Basics.tex Mon Jul 30 14:11:29 2012 +0200
@@ -100,7 +100,7 @@
You should not try to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} manually. Also
note that the Isabelle executables either have to be run from their
original location in the distribution directory, or via the
- executable objects created by the \hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}} utility. Symbolic
+ executable objects created by the \hyperlink{tool.install}{\mbox{\isa{\isatool{install}}}} tool. Symbolic
links are admissible, but a plain copy of the \verb|$ISABELLE_HOME/bin| files will not work!
\item The file \verb|$ISABELLE_HOME/etc/settings| is run as a
@@ -153,8 +153,8 @@
\end{itemize}
\medskip Note that the settings environment may be inspected with
- the Isabelle tool \hyperlink{tool.getenv}{\mbox{\isa{\isatt{getenv}}}}. This might help to figure out the
- effect of complex settings scripts.%
+ the \hyperlink{tool.getenv}{\mbox{\isa{\isatool{getenv}}}} tool. This might help to figure out the effect
+ of complex settings scripts.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -251,11 +251,11 @@
\verb|HOL|.
\item[\indexdef{}{setting}{ISABELLE\_LINE\_EDITOR}\hypertarget{setting.ISABELLE-LINE-EDITOR}{\hyperlink{setting.ISABELLE-LINE-EDITOR}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LINE{\isaliteral{5F}{\isacharunderscore}}EDITOR}}}}}] specifies the default
- line editor for the \indexref{}{tool}{tty}\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}} interface.
+ line editor for the \indexref{}{tool}{tty}\hyperlink{tool.tty}{\mbox{\isa{\isatool{tty}}}} interface.
\item[\indexdef{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hypertarget{setting.ISABELLE-USEDIR-OPTIONS}{\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}USEDIR{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}}] is implicitly prefixed
- to the command line of any \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} invocation. This
- typically contains compilation options for object-logics --- \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} is the basic utility for managing logic sessions (cf.\ the
+ to the command line of any \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} invocation. This
+ typically contains compilation options for object-logics --- \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} is the basic tool for managing logic sessions (cf.\ the
\verb|IsaMakefile|s in the distribution).
\item[\indexdef{}{setting}{ISABELLE\_LATEX}\hypertarget{setting.ISABELLE-LATEX}{\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LATEX}}}}}, \indexdef{}{setting}{ISABELLE\_PDFLATEX}\hypertarget{setting.ISABELLE-PDFLATEX}{\hyperlink{setting.ISABELLE-PDFLATEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PDFLATEX}}}}}, \indexdef{}{setting}{ISABELLE\_BIBTEX}\hypertarget{setting.ISABELLE-BIBTEX}{\hyperlink{setting.ISABELLE-BIBTEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BIBTEX}}}}}, \indexdef{}{setting}{ISABELLE\_DVIPS}\hypertarget{setting.ISABELLE-DVIPS}{\hyperlink{setting.ISABELLE-DVIPS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DVIPS}}}}}] refer to {\LaTeX} related tools for Isabelle
@@ -489,7 +489,7 @@
\medskip Note that manual session management like this does
\emph{not} provide proper setup for theory presentation. This would
- require the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility.
+ require \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}.
\bigskip The next example demonstrates batch execution of Isabelle.
We retrieve the \verb|Main| theory value from the theory loader
--- a/doc-src/System/Thy/document/Interfaces.tex Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/System/Thy/document/Interfaces.tex Mon Jul 30 14:11:29 2012 +0200
@@ -27,7 +27,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{jedit}\hypertarget{tool.jedit}{\hyperlink{tool.jedit}{\mbox{\isa{\isatt{jedit}}}}} tool invokes a version of jEdit that has
+The \indexdef{}{tool}{jedit}\hypertarget{tool.jedit}{\hyperlink{tool.jedit}{\mbox{\isa{\isatool{jedit}}}}} tool invokes a version of jEdit that has
been augmented with some components to provide a fully-featured
Prover IDE (based on Isabelle/Scala):
\begin{ttbox}
@@ -69,7 +69,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and
+The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatool{emacs}}}}} tool invokes a version of Emacs and
Proof General \cite{proofgeneral} within the regular Isabelle
settings environment (\secref{sec:settings}). This is more
convenient than starting Emacs separately, loading the Proof General
@@ -104,7 +104,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} tool runs the Isabelle process interactively
+The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatool{tty}}}}} tool runs the Isabelle process interactively
within a plain terminal session:
\begin{ttbox}
Usage: isabelle tty [OPTIONS]
@@ -142,9 +142,8 @@
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
- \verb|-g| of \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} creates
- graph presentations in batch mode for inclusion in session
- documents.%
+ \verb|-g| of \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} creates graph presentations
+ in batch mode for inclusion in session documents.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -153,11 +152,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The stand-alone version of the graph browser is wrapped up as an
- Isabelle tool called \indexdef{}{tool}{browser}\hypertarget{tool.browser}{\hyperlink{tool.browser}{\mbox{\isa{\isatt{browser}}}}}:
-
+The stand-alone version of the graph browser is wrapped up as
+ \indexdef{}{tool}{browser}\hypertarget{tool.browser}{\hyperlink{tool.browser}{\mbox{\isa{\isatool{browser}}}}}:
\begin{ttbox}
-Usage: browser [OPTIONS] [GRAPHFILE]
+Usage: isabelle browser [OPTIONS] [GRAPHFILE]
Options are:
-b Admin/build only
--- a/doc-src/System/Thy/document/Misc.tex Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/System/Thy/document/Misc.tex Mon Jul 30 14:11:29 2012 +0200
@@ -33,10 +33,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{display}\hypertarget{tool.display}{\hyperlink{tool.display}{\mbox{\isa{\isatt{display}}}}} utility displays documents in DVI or PDF
+The \indexdef{}{tool}{display}\hypertarget{tool.display}{\hyperlink{tool.display}{\mbox{\isa{\isatool{display}}}}} tool displays documents in DVI or PDF
format:
\begin{ttbox}
-Usage: display [OPTIONS] FILE
+Usage: isabelle display [OPTIONS] FILE
Options are:
-c cleanup -- remove FILE after use
@@ -55,9 +55,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{doc}\hypertarget{tool.doc}{\hyperlink{tool.doc}{\mbox{\isa{\isatt{doc}}}}} utility displays online documentation:
+The \indexdef{}{tool}{doc}\hypertarget{tool.doc}{\hyperlink{tool.doc}{\mbox{\isa{\isatool{doc}}}}} tool displays online documentation:
\begin{ttbox}
-Usage: doc [DOC]
+Usage: isabelle doc [DOC]
View Isabelle documentation DOC, or show list of available documents.
\end{ttbox}
@@ -78,10 +78,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{env}\hypertarget{tool.env}{\hyperlink{tool.env}{\mbox{\isa{\isatt{env}}}}} utility is a direct wrapper for the
- standard \verb|/usr/bin/env| command on POSIX systems,
- running within the Isabelle settings environment
- (\secref{sec:settings}).
+The \indexdef{}{tool}{env}\hypertarget{tool.env}{\hyperlink{tool.env}{\mbox{\isa{\isatool{env}}}}} tool is a direct wrapper for the standard
+ \verb|/usr/bin/env| command on POSIX systems, running within
+ the Isabelle settings environment (\secref{sec:settings}).
The command-line arguments are that of the underlying version of
\verb|env|. For example, the following invokes an instance of
@@ -97,7 +96,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{findlogics}\hypertarget{tool.findlogics}{\hyperlink{tool.findlogics}{\mbox{\isa{\isatt{findlogics}}}}} utility traverses all directories
+The \indexdef{}{tool}{findlogics}\hypertarget{tool.findlogics}{\hyperlink{tool.findlogics}{\mbox{\isa{\isatool{findlogics}}}}} tool traverses all directories
specified in \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PATH}}}}, looking for Isabelle logic
images. Its usage is:
\begin{ttbox}
@@ -120,9 +119,9 @@
\begin{isamarkuptext}%
The Isabelle settings environment --- as provided by the
site-default and user-specific settings files --- can be inspected
- with the \indexdef{}{tool}{getenv}\hypertarget{tool.getenv}{\hyperlink{tool.getenv}{\mbox{\isa{\isatt{getenv}}}}} utility:
+ with the \indexdef{}{tool}{getenv}\hypertarget{tool.getenv}{\hyperlink{tool.getenv}{\mbox{\isa{\isatool{getenv}}}}} tool:
\begin{ttbox}
-Usage: getenv [OPTIONS] [VARNAMES ...]
+Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
Options are:
-a display complete environment
@@ -182,12 +181,12 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-By default, the main Isabelle binaries (\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}
- etc.) are just run from their location within the distribution
- directory, probably indirectly by the shell through its \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}. Other schemes of installation are supported by the
- \indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}}} utility:
+By default, the main Isabelle binaries (\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} etc.) are just run from their location within the
+ distribution directory, probably indirectly by the shell through its
+ \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}. Other schemes of installation are supported by the
+ \indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatool{install}}}}} tool:
\begin{ttbox}
-Usage: install [OPTIONS]
+Usage: isabelle install [OPTIONS]
Options are:
-d DISTDIR use DISTDIR as Isabelle distribution
@@ -218,10 +217,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{logo}\hypertarget{tool.logo}{\hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}} utility creates any instance of the generic
+The \indexdef{}{tool}{logo}\hypertarget{tool.logo}{\hyperlink{tool.logo}{\mbox{\isa{\isatool{logo}}}}} tool creates any instance of the generic
Isabelle logo as an Encapsuled Postscript file (EPS):
\begin{ttbox}
-Usage: logo [OPTIONS] NAME
+Usage: isabelle logo [OPTIONS] NAME
Create instance NAME of the Isabelle logo (as EPS).
@@ -230,7 +229,8 @@
-q quiet mode
\end{ttbox}
You are encouraged to use this to create a derived logo for your
- Isabelle project. For example, \verb|isabelle| \hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}~\verb|Bali| creates \verb|isabelle_bali.eps|.%
+ Isabelle project. For example, \hyperlink{tool.logo}{\mbox{\isa{\isatool{logo}}}}~\verb|Bali|
+ creates \verb|isabelle_bali.eps|.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -239,10 +239,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The Isabelle \indexdef{}{tool}{make}\hypertarget{tool.make}{\hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}} utility is a very simple wrapper for
+The \indexdef{}{tool}{make}\hypertarget{tool.make}{\hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}}} tool is a very simple wrapper for
ordinary Unix \hyperlink{executable.make}{\mbox{\isa{\isatt{make}}}}:
\begin{ttbox}
-Usage: make [ARGS ...]
+Usage: isabelle make [ARGS ...]
Compile the logic in current directory using IsaMakefile.
ARGS are directly passed to the system make program.
@@ -251,7 +251,7 @@
Note that the Isabelle settings environment is also active. Thus one
may refer to its values within the \verb|IsaMakefile|, e.g.\
\verb|$(ISABELLE_OUTPUT)|. Furthermore, programs started from
- the make file also inherit this environment. Typically, \verb|IsaMakefile|s defer the real work to the \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility.
+ the make file also inherit this environment. Typically, \verb|IsaMakefile|s defer the real work to \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}.
\medskip The basic \verb|IsaMakefile| convention is that the
default target builds the actual logic, including its parents if
@@ -278,17 +278,17 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{makeall}\hypertarget{tool.makeall}{\hyperlink{tool.makeall}{\mbox{\isa{\isatt{makeall}}}}} utility applies Isabelle make to any
+The \indexdef{}{tool}{makeall}\hypertarget{tool.makeall}{\hyperlink{tool.makeall}{\mbox{\isa{\isatool{makeall}}}}} tool applies Isabelle make to any
Isabelle component (cf.\ \secref{sec:components}) that contains an
\verb|IsaMakefile|:
\begin{ttbox}
-Usage: makeall [ARGS ...]
+Usage: isabelle makeall [ARGS ...]
Apply isabelle make to all components with IsaMakefile (passing ARGS).
\end{ttbox}
The arguments \verb|ARGS| are just passed verbatim to each
- \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} invocation.%
+ \hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}} invocation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -297,9 +297,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{print}\hypertarget{tool.print}{\hyperlink{tool.print}{\mbox{\isa{\isatt{print}}}}} utility prints documents:
+The \indexdef{}{tool}{print}\hypertarget{tool.print}{\hyperlink{tool.print}{\mbox{\isa{\isatool{print}}}}} tool prints documents:
\begin{ttbox}
-Usage: print [OPTIONS] FILE
+Usage: isabelle print [OPTIONS] FILE
Options are:
-c cleanup -- remove FILE after use
@@ -317,13 +317,13 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{unsymbolize}\hypertarget{tool.unsymbolize}{\hyperlink{tool.unsymbolize}{\mbox{\isa{\isatt{unsymbolize}}}}} utility tunes Isabelle theory sources to
+The \indexdef{}{tool}{unsymbolize}\hypertarget{tool.unsymbolize}{\hyperlink{tool.unsymbolize}{\mbox{\isa{\isatool{unsymbolize}}}}} tool tunes Isabelle theory sources to
improve readability for plain ASCII output (e.g.\ in email
- communication). Most notably, \hyperlink{tool.unsymbolize}{\mbox{\isa{\isatt{unsymbolize}}}} replaces awkward
+ communication). Most notably, \hyperlink{tool.unsymbolize}{\mbox{\isa{\isatool{unsymbolize}}}} replaces awkward
arrow symbols such as \verb|\|\verb|<Longrightarrow>|
by \verb|==>|.
\begin{ttbox}
-Usage: unsymbolize [FILES|DIRS...]
+Usage: isabelle unsymbolize [FILES|DIRS...]
Recursively find .thy/.ML files, removing unreadable symbol names.
Note: this is an ad-hoc script; there is no systematic way to replace
@@ -339,7 +339,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{version}\hypertarget{tool.version}{\hyperlink{tool.version}{\mbox{\isa{\isatt{version}}}}} utility displays Isabelle version information:
+The \indexdef{}{tool}{version}\hypertarget{tool.version}{\hyperlink{tool.version}{\mbox{\isa{\isatool{version}}}}} tool displays Isabelle version information:
\begin{ttbox}
Usage: isabelle version [OPTIONS]
@@ -362,7 +362,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{yxml}\hypertarget{tool.yxml}{\hyperlink{tool.yxml}{\mbox{\isa{\isatt{yxml}}}}} tool converts a standard XML document (stdin)
+The \indexdef{}{tool}{yxml}\hypertarget{tool.yxml}{\hyperlink{tool.yxml}{\mbox{\isa{\isatool{yxml}}}}} tool converts a standard XML document (stdin)
to the much simpler and more efficient YXML format of Isabelle
(stdout). The YXML format is defined as follows.
--- a/doc-src/System/Thy/document/Presentation.tex Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex Mon Jul 30 14:11:29 2012 +0200
@@ -31,35 +31,37 @@
(e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions
in leaf positions (usually without a separate image).
- The Isabelle tools \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} and \indexref{}{tool}{make}\hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} provide
- the primary means for managing Isabelle sessions, including proper
- setup for presentation. Here the \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} tool takes care
- to let \indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} process run any
- additional stages required for document preparation, notably the
- tools \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} and \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}}. The complete tool
- chain for managing batch-mode Isabelle sessions is illustrated in
+ The tools \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}} and \indexref{}{tool}{make}\hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}} provide the primary
+ means for managing Isabelle sessions, including proper setup for
+ presentation. Here \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} takes care to let
+ \indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} process run any additional
+ stages required for document preparation, notably the tools
+ \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}} and \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}}. The complete tool chain
+ for managing batch-mode Isabelle sessions is illustrated in
\figref{fig:session-tools}.
\begin{figure}[htbp]
\begin{center}
\begin{tabular}{lp{0.6\textwidth}}
- \verb|isabelle| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} & invoked once by the user
- to create the initial source setup (common \verb|IsaMakefile| plus a single session directory); \\
+ \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}} & invoked once by the user to create the
+ initial source setup (common \verb|IsaMakefile| plus a
+ single session directory); \\
- \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} & invoked repeatedly by the
- user to keep session output up-to-date (HTML, documents etc.); \\
+ \hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}} & invoked repeatedly by the user to keep session
+ output up-to-date (HTML, documents etc.); \\
- \verb|isabelle| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} & part of the standard
- \verb|IsaMakefile| entry of a session; \\
+ \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} & part of the standard \verb|IsaMakefile|
+ entry of a session; \\
- \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} & run through \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}; \\
+ \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} & run through \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}; \\
- \verb|isabelle| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} & run by the Isabelle
- process if document preparation is enabled; \\
+ \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}} & run by the Isabelle process if document
+ preparation is enabled; \\
- \verb|isabelle| \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} & universal {\LaTeX} tool
- wrapper invoked multiple times by \verb|isabelle| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}; also useful for manual experiments; \\
+ \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}} & universal {\LaTeX} tool wrapper invoked
+ multiple times by \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}}; also useful for manual
+ experiments; \\
\end{tabular}
\caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
@@ -96,20 +98,18 @@
The easiest way to let Isabelle generate theory browsing information
for existing sessions is to append ``\verb|-i true|'' to the
- \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}USEDIR{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}} before invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}. For example, add something like this to
- your Isabelle settings file
+ \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}USEDIR{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}} before invoking \hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}}.
+ 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 \verb|~~/src/FOL| directory and run
- \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle|
- \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|. The presentation output will appear
- in \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
- something like \verb|~/.isabelle/IsabelleXXXX/browser_info/FOL|. Note that option
- \verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
- more explicit about such details.
+ \hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}}, or even \hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}}~\verb|all|. The
+ presentation output will appear in \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to something like
+ \verb|~/.isabelle/IsabelleXXXX/browser_info/FOL|. Note that
+ option \verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} more explicit about such details.
Many standard Isabelle sessions (such as \verb|~~/src/HOL/ex|)
also provide actual printable documents. These are prepared
@@ -145,21 +145,18 @@
\end{ttbox}
This assumes that directory \verb|Foo| contains some \verb|ROOT.ML| file to load all your theories, and HOL is your parent
- logic image (\verb|isabelle| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{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
- of HTML data by giving \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} a \verb|-P| option like
- this:
+ logic image (\indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatool{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 of HTML data by giving \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} a \verb|-P| option like this:
\begin{ttbox}
isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
\end{ttbox}
- \medskip For production use, the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} tool is usually
- invoked in an appropriate \verb|IsaMakefile|, via the Isabelle
- \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} tool. There is a separate \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool to
- provide easy setup of all this, with only minimal manual editing
- required.
+ \medskip For production use, \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} is usually invoked in an
+ appropriate \verb|IsaMakefile|, via \hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}}. There is a
+ separate \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}} tool to provide easy setup of all this, with
+ only minimal manual editing required.
\begin{ttbox}
isabelle mkdir HOL Foo && isabelle make
\end{ttbox}
@@ -174,15 +171,15 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{mkdir}\hypertarget{tool.mkdir}{\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}} utility prepares Isabelle session source
+The \indexdef{}{tool}{mkdir}\hypertarget{tool.mkdir}{\hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}}} tool prepares Isabelle session source
directories, including a sensible default setup of \verb|IsaMakefile|, \verb|ROOT.ML|, and a \verb|document|
directory with a minimal \verb|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 \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} is:
+ document preparation. The usage of \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}} is:
\begin{ttbox}
-Usage: mkdir [OPTIONS] [LOGIC] NAME
+Usage: isabelle mkdir [OPTIONS] [LOGIC] NAME
Options are:
-I FILE alternative IsaMakefile output
@@ -194,12 +191,12 @@
with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
\end{ttbox}
- The \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool is conservative in the sense that any
+ The \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}} tool is conservative in the sense that any
existing \verb|IsaMakefile| etc.\ is left unchanged. Thus it
is safe to invoke it multiple times, although later runs may not
have the desired effect.
- Note that \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} is unable to change \verb|IsaMakefile|
+ Note that \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}} is unable to change \verb|IsaMakefile|
incrementally --- manual changes are required for multiple
sub-sessions. On order to get an initial working session, the only
editing needed is to add appropriate \verb|use_thy| calls to the
@@ -214,7 +211,7 @@
\begin{isamarkuptext}%
The \verb|-I| option specifies an alternative to \verb|IsaMakefile| for dependencies. Note that ``\verb|-|'' refers
to \emph{stdout}, i.e.\ ``\verb|-I-|'' provides an easy way
- to peek at \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}'s idea of \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} setup required for
+ to peek at \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}}'s idea of \hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}} setup required for
some particular of Isabelle session.
\medskip The \verb|-P| option includes a target for the
@@ -228,7 +225,7 @@
\verb|IsaMakefile| would be placed into a separate directory
\verb|NAME|, rather than the current one. See
\secref{sec:tool-usedir} for further information on \emph{build
- mode} vs.\ \emph{example mode} of the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility.
+ mode} vs.\ \emph{example mode} of \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}.
\medskip The \verb|-q| option enables quiet mode, suppressing
further notes on how to proceed.%
@@ -249,19 +246,19 @@
\noindent The theory sources should be put into the \verb|Foo|
directory, and its \verb|ROOT.ML| should be edited to load all
- required theories. Invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} again
- would run the whole session, generating browser information and the
- document automatically. The \verb|IsaMakefile| is typically
- tuned manually later, e.g.\ adding source dependencies, or changing
- the options passed to \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}.
+ required theories. Invoking \hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}} again would run the whole
+ session, generating browser information and the document
+ automatically. The \verb|IsaMakefile| is typically tuned
+ manually later, e.g.\ adding source dependencies, or changing the
+ options passed to \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}.
\medskip Large projects may demand further sessions, potentially
with separate logic images being created. This usually requires
manual editing of the generated \verb|IsaMakefile|, which is
meant to cover all of the sub-session directories at the same time
(this is the deeper reasong why \verb|IsaMakefile| is not made
- part of the initial session directory created by \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}). See \verb|~~/src/HOL/IsaMakefile| for
- a full-blown example.%
+ part of the initial session directory created by \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}}).
+ See \verb|~~/src/HOL/IsaMakefile| for a full-blown example.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -270,10 +267,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{usedir}\hypertarget{tool.usedir}{\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}} utility builds object-logic images, or runs
- example sessions based on existing logics. Its usage is:
+The \indexdef{}{tool}{usedir}\hypertarget{tool.usedir}{\hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}} tool builds object-logic images, or
+ runs example sessions based on existing logics. Its usage is:
\begin{ttbox}
-Usage: usedir [OPTIONS] LOGIC NAME
+Usage: isabelle usedir [OPTIONS] LOGIC NAME
Options are:
-C BOOL copy existing document directory to -D PATH (default true)
@@ -308,9 +305,9 @@
\end{ttbox}
Note that the value of the \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}USEDIR{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}
- setting is implicitly prefixed to \emph{any} \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
+ setting is implicitly prefixed to \emph{any} \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}
call. Since the \verb|IsaMakefile|s of all object-logics
- distributed with Isabelle just invoke \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} for the real
+ distributed with Isabelle just invoke \hyperlink{tool.usedir}{\mbox{\isa{\isatool{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.%
@@ -326,13 +323,13 @@
mode} (enabled through the \verb|-b| option) and
\emph{example mode} (default).
- Calling \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} with \verb|-b| runs \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} with input image \verb|LOGIC| and output to
+ Calling \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} with \verb|-b| runs \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} with input image \verb|LOGIC| and output to
\verb|NAME|, as provided on the command line. This will be a
batch session, running \verb|ROOT.ML| from the current
directory and then quitting. It is assumed that \verb|ROOT.ML|
contains all ML commands required to build the logic.
- In example mode, \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} runs a read-only session of
+ In example mode, \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} runs a read-only session of
\verb|LOGIC| and automatically runs \verb|ROOT.ML| from
within directory \verb|NAME|. It assumes that this file
contains appropriate ML commands to run the desired examples.
@@ -358,8 +355,8 @@
\secref{sec:tool-latex} for more details.
\medskip The \verb|-V| option declares alternative document
- variants, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool). The
- standard document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end
+ variants, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}}). The standard
+ document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end
commands, proof body texts, and ML code will be presented
faithfully. An alternative variant ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
original text by a short place-holder. The form ``\isa{name}\verb|=-|,'' means to remove document \isa{name} from
@@ -377,9 +374,9 @@
\medskip The \verb|-D| option causes the generated document
sources to be dumped at location \verb|PATH|; this path is
relative to the session's main directory. If the \verb|-C|
- option is true, this will include a copy of an existing \verb|document| directory as provided by the user. For example,
- \verb|isabelle| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}~\verb|-D generated HOL|\isasep\isanewline%
-\verb| Foo| produces a complete set of document sources at \verb|Foo/generated|. Subsequent invocation of \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|Foo/generated| (see also
+ option is true, this will include a copy of an existing \verb|document| directory as provided by the user. For example, \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}~\verb|-D generated HOL Foo| produces a complete set
+ of document sources at \verb|Foo/generated|. Subsequent
+ invocation of \hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}}~\verb|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.
@@ -414,7 +411,7 @@
performance bottle-necks, e.g.\ due to excessive wait states when
locking critical code sections.
- \medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
+ \medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend
on others. For example, consider \verb|Pure/FOL/ex|, which
refers to the examples of FOL, which in turn is built upon Pure.
@@ -430,10 +427,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
- object-logics as a model for your own developments. For example,
- see \verb|~~/src/FOL/IsaMakefile|. The Isabelle \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool creates \verb|IsaMakefile|s with proper invocation
- of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} as well.%
+Refer to the \verb|IsaMakefile|s of the Isabelle
+ distribution's object-logics as a model for your own developments.
+ For example, see \verb|~~/src/FOL/IsaMakefile|. The \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}} tool creates \verb|IsaMakefile|s with proper invocation
+ of \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} as well.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -443,11 +440,11 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{document}\hypertarget{tool.document}{\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}} utility prepares logic session documents,
- processing the sources both as provided by the user and generated by
- Isabelle. Its usage is:
+The \indexdef{}{tool}{document}\hypertarget{tool.document}{\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}}} tool prepares logic session
+ documents, processing the sources both as provided by the user and
+ generated by Isabelle. Its usage is:
\begin{ttbox}
-Usage: document [OPTIONS] [DIR]
+Usage: isabelle document [OPTIONS] [DIR]
Options are:
-c cleanup -- be aggressive in removing old stuff
@@ -461,13 +458,13 @@
\end{ttbox}
This tool is usually run automatically as part of the corresponding
Isabelle batch process, provided document preparation has been
- enabled (cf.\ the \verb|-d| option of the \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
- tool). It may be manually invoked on the generated browser
- information document output as well, e.g.\ in case of errors
- encountered in the batch run.
+ enabled (cf.\ the \verb|-d| option of \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}).
+ It may be manually invoked on the generated browser information
+ document output as well, e.g.\ in case of errors encountered in the
+ batch run.
- \medskip The \verb|-c| option tells the \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool
- to dispose the document sources after successful operation. This is
+ \medskip The \verb|-c| option tells \hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}} to
+ dispose the document sources after successful operation. This is
the right thing to do for sources generated by an Isabelle process,
but take care of your files in manual document preparation!
@@ -488,8 +485,8 @@
final document --- apart from the actual theories which are
generated by Isabelle.
- \medskip For most practical purposes, the \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool is
- smart enough to create any of the specified output formats, taking
+ \medskip For most practical purposes, \hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}} is smart
+ enough to create any of the specified output formats, taking
\verb|root.tex| supplied by the user as a starting point. This
even includes multiple runs of {\LaTeX} to accommodate references
and bibliographies (the latter assumes \verb|root.bib| within
@@ -511,8 +508,8 @@
The {\LaTeX} versions of the theories require some macros defined in
\verb|~~/lib/texinputs/isabelle.sty|. Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
- the underlying Isabelle \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} tool already includes an
- appropriate path specification for {\TeX} inputs.
+ the underlying \hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}} already includes an appropriate path
+ specification for {\TeX} inputs.
If the text contains any references to Isabelle symbols (such as
\verb|\|\verb|<forall>|) then \verb|isabellesym.sty| should be included as well. This package
@@ -526,15 +523,12 @@
bookmarks), we recommend to include \verb|~~/lib/texinputs/pdfsetup.sty| as well.
\medskip As a final step of document preparation within Isabelle,
- \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|-c| is run on the
- resulting \verb|document| directory. Thus the actual output
- document is built and installed in its proper place (as linked by
- the session's \verb|index.html| if option \verb|-i| of
- \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{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 \verb|-D| to the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility
- when running the session.%
+ \hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}}~\verb|-c| is run on the resulting \verb|document| directory. Thus the actual output document is built and
+ installed in its proper place (as linked by the session's \verb|index.html| if option \verb|-i| of \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatool{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
+ \verb|-D| to \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} when running the session.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -544,10 +538,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{latex}\hypertarget{tool.latex}{\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}}} utility provides the basic interface for
+The \indexdef{}{tool}{latex}\hypertarget{tool.latex}{\hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}}} tool provides the basic interface for
Isabelle document preparation. Its usage is:
\begin{ttbox}
-Usage: latex [OPTIONS] [FILE]
+Usage: isabelle latex [OPTIONS] [FILE]
Options are:
-o FORMAT specify output format: dvi (default), dvi.gz, ps,
@@ -566,7 +560,7 @@
The \verb|sty| output format causes the Isabelle style files to
be updated from the distribution. This is useful in special
situations where the document sources are to be processed another
- time by separate tools (cf.\ option \verb|-D| of the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility).
+ time by separate tools (cf.\ option \verb|-D| of \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}).
The \verb|syms| output is for internal use; it generates lists
of symbols that are available without loading additional {\LaTeX}
@@ -579,12 +573,13 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Invoking \verb|isabelle| \hyperlink{tool.latex}{\mbox{\isa{\isatt{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 \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}, see the runtime error message for details.
- This enables users to inspect {\LaTeX} runs in further detail, e.g.\
- like this:
+Invoking \hyperlink{tool.latex}{\mbox{\isa{\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 \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}},
+ see the runtime error message for details. This enables users to
+ inspect {\LaTeX} runs in further detail, e.g.\ like this:
+
\begin{ttbox}
cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
isabelle latex -o pdf
--- a/doc-src/System/Thy/document/Scala.tex Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/System/Thy/document/Scala.tex Mon Jul 30 14:11:29 2012 +0200
@@ -37,8 +37,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The Isabelle \indexdef{}{tool}{java}\hypertarget{tool.java}{\hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}}} utility is a direct wrapper for
- the Java Runtime Environment, within the regular Isabelle settings
+The \indexdef{}{tool}{java}\hypertarget{tool.java}{\hyperlink{tool.java}{\mbox{\isa{\isatool{java}}}}} tool is a direct wrapper for the Java
+ Runtime Environment, within the regular Isabelle settings
environment (\secref{sec:settings}). The command line arguments are
that of the underlying Java version. It is run in \verb|-server| mode if possible, to improve performance (at the cost of
extra startup time).
@@ -62,9 +62,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The Isabelle \indexdef{}{tool}{scala}\hypertarget{tool.scala}{\hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}}} utility is a direct wrapper for
- the Scala toplevel; see also \hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}} above. The command line
- arguments are that of the underlying Scala version.
+The \indexdef{}{tool}{scala}\hypertarget{tool.scala}{\hyperlink{tool.scala}{\mbox{\isa{\isatool{scala}}}}} tool is a direct wrapper for the Scala
+ toplevel; see also \hyperlink{tool.java}{\mbox{\isa{\isatool{java}}}} above. The command line arguments
+ are that of the underlying Scala version.
This allows to interact with Isabelle/Scala in TTY mode like this:
\begin{alltt}
@@ -80,9 +80,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The Isabelle \indexdef{}{tool}{scalac}\hypertarget{tool.scalac}{\hyperlink{tool.scalac}{\mbox{\isa{\isatt{scalac}}}}} utility is a direct wrapper
- for the Scala compiler; see also \hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}} above. The command
- line arguments are that of the underlying Scala version.
+The \indexdef{}{tool}{scalac}\hypertarget{tool.scalac}{\hyperlink{tool.scalac}{\mbox{\isa{\isatool{scalac}}}}} tool is a direct wrapper for the Scala
+ compiler; see also \hyperlink{tool.scala}{\mbox{\isa{\isatool{scala}}}} above. The command line arguments
+ are that of the underlying Scala version.
This allows to compile further Scala modules, depending on existing
Isabelle/Scala functionality. The resulting class or jar files can
--- a/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 14:11:29 2012 +0200
@@ -265,14 +265,15 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \indexdef{}{tool}{build}\hypertarget{tool.build}{\hyperlink{tool.build}{\mbox{\isa{\isatt{build}}}}} utility invokes the build process for
+The \indexdef{}{tool}{build}\hypertarget{tool.build}{\hyperlink{tool.build}{\mbox{\isa{\isatool{build}}}}} tool invokes the build process for
Isabelle sessions. It manages dependencies between sessions,
related sources of theories and auxiliary files, and target heap
images. Accordingly, it runs instances of the prover process with
optional document preparation. Its command-line usage
is:\footnote{Isabelle/Scala provides the same functionality via
\texttt{isabelle.Build.build}.}
-\begin{ttbox} Usage: isabelle build [OPTIONS] [SESSIONS ...]
+\begin{ttbox}
+Usage: isabelle build [OPTIONS] [SESSIONS ...]
Options are:
-a select all sessions
--- a/doc-src/antiquote_setup.ML Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/antiquote_setup.ML Mon Jul 30 14:11:29 2012 +0200
@@ -208,7 +208,7 @@
entity_antiqs no_check "isatt" "system option" #>
entity_antiqs no_check "" "inference" #>
entity_antiqs no_check "isatt" "executable" #>
- entity_antiqs (K check_tool) "isatt" "tool" #>
+ entity_antiqs (K check_tool) "isatool" "tool" #>
entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq)
"" Isabelle_Markup.ML_antiquotationN;
--- a/doc-src/isar.sty Mon Jul 30 13:48:56 2012 +0200
+++ b/doc-src/isar.sty Mon Jul 30 14:11:29 2012 +0200
@@ -5,6 +5,7 @@
\newcommand{\indexref}[3]{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)}}{\index{#3 (#1\ #2)}}}
\newcommand{\isatt}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt #1}}
+\newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt isabelle #1}}
\newcommand{\indexoutertoken}[1]{\indexdef{}{syntax}{#1}}
\newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}