src/Doc/System/Presentation.thy

added function "List.extract"

theory Presentation
imports Base
begin

chapter {* Presenting theories \label{ch:present} *}

text {* Isabelle provides several ways to present the outcome of
  formal developments, including WWW-based browsable libraries or
  actual printable documents.  Presentation is centered around the
  concept of \emph{sessions} (\chref{ch:session}).  The global session
  structure is that of a tree, with Isabelle Pure at its root, further
  object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and
  application sessions further on in the hierarchy.

  The tools @{tool_ref mkroot} and @{tool_ref build} provide the
  primary means for managing Isabelle sessions, including proper setup
  for presentation; @{tool build} takes care to have @{executable_ref
  "isabelle-process"} run any additional stages required for document
  preparation, notably the @{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}}

      @{tool_ref mkroot} & invoked once by the user to initialize the
      session @{verbatim ROOT} with optional @{verbatim document}
      directory; \\

      @{tool_ref build} & invoked repeatedly by the user to keep
      session output up-to-date (HTML, documents etc.); \\

      @{executable "isabelle-process"} & run through @{tool_ref
      build}; \\

      @{tool_ref document} & run by the Isabelle process if document
      preparation is enabled; \\

      @{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}
  \end{center}
  \end{figure}
*}


section {* Generating theory browser information \label{sec:info} *}

text {*
  \index{theory browsing information|bold}

  As a side-effect of building sessions, Isabelle is able to generate
  theory browsing information, including HTML documents that show the
  theory sources and the relationship with its ancestors and
  descendants.  Besides the HTML file that is generated for every
  theory, Isabelle stores links to all theories of a session in an
  index file.  As a second hierarchy, groups of sessions are organized
  as \emph{chapters}, with a separate index.  Note that the implicit
  tree structure of the session build hierarchy is \emph{not} relevant
  for the presentation.

  Isabelle also generates graph files that represent the theory
  dependencies within a session.  There is a graph browser Java applet
  embedded in the generated HTML pages, and also a stand-alone
  application that allows browsing theory graphs without having to
  start a WWW client first.  The latter version also includes features
  such as generating Postscript files, which are not available in the
  applet version.  See \secref{sec:browse} for further information.

  \medskip

  The easiest way to let Isabelle generate theory browsing information
  for existing sessions is to invoke @{tool build} with suitable
  options:

\begin{ttbox}
isabelle build -o browser_info -v -c FOL
\end{ttbox}

  The presentation output will appear in @{verbatim
  "$ISABELLE_BROWSER_INFO/FOL/FOL"} as reported by the above verbose
  invocation of the build process.

  Many Isabelle sessions (such as @{verbatim "HOL-Library"} in @{file
  "~~/src/HOL/Library"}) also provide actual printable documents.
  These are prepared automatically as well if enabled like this:
\begin{ttbox}
isabelle build -o browser_info -o document=pdf -v -c HOL-Library
\end{ttbox}

  Enabling both browser info and document preparation simultaneously
  causes an appropriate ``document'' link to be included in the HTML
  index.  Documents may be generated independently of browser
  information as well, see \secref{sec:tool-document} for further
  details.

  \bigskip The theory browsing information is stored in a
  sub-directory directory determined by the @{setting_ref
  ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the
  session chapter and identifier.  In order to present Isabelle
  applications on the web, the corresponding subdirectory from
  @{setting ISABELLE_BROWSER_INFO} can be put on a WWW server.  *}

section {* Preparing session root directories \label{sec:tool-mkroot} *}

text {* The @{tool_def mkroot} tool configures a given directory as
  session root, with some @{verbatim ROOT} file and optional document
  source directory.  Its usage is:
\begin{ttbox}
Usage: isabelle mkroot [OPTIONS] [DIR]

  Options are:
    -d           enable document preparation
    -n NAME      alternative session name (default: DIR base name)

  Prepare session root DIR (default: current directory).
\end{ttbox}

  The results are placed in the given directory @{text dir}, which
  refers to the current directory by default.  The @{tool mkroot} tool
  is conservative in the sense that it does not overwrite existing
  files or directories.  Earlier attempts to generate a session root
  need to be deleted manually.

  \medskip Option @{verbatim "-d"} indicates that the session shall be
  accompanied by a formal document, with @{text DIR}@{verbatim
  "/document/root.tex"} as its {\LaTeX} entry point (see also
  \chref{ch:present}).

  Option @{verbatim "-n"} allows to specify an alternative session
  name; otherwise the base name of the given directory is used.

  \medskip The implicit Isabelle settings variable @{setting
  ISABELLE_LOGIC} specifies the parent session, and @{setting
  ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled
  into the generated @{verbatim ROOT} file.  *}


subsubsection {* Examples *}

text {* Produce session @{verbatim Test} (with document preparation)
  within a separate directory of the same name:
\begin{ttbox}
isabelle mkroot -d Test && isabelle build -D Test
\end{ttbox}

  \medskip Upgrade the current directory into a session ROOT with
  document preparation, and build it:
\begin{ttbox}
isabelle mkroot -d && isabelle build -D .
\end{ttbox}
*}


section {* Preparing Isabelle session documents
  \label{sec:tool-document} *}

text {* The @{tool_def document} tool prepares logic session
  documents, processing the sources as provided by the user and
  generated by Isabelle.  Its usage is:
\begin{ttbox}
Usage: isabelle document [OPTIONS] [DIR]

  Options are:
    -c           cleanup -- be aggressive in removing old stuff
    -n NAME      specify document name (default 'document')
    -o FORMAT    specify output format: pdf (default), dvi
    -t TAGS      specify tagged region markup

  Prepare the theory session document in DIR (default 'document')
  producing the specified output format.
\end{ttbox}
  This tool is usually run automatically as part of the Isabelle build
  process, provided document preparation has been enabled via suitable
  options.  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 @{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!

  \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify
  the final output file name and format, the default is ``@{verbatim
  document.dvi}''.  Note that the result will appear in the parent of
  the target @{verbatim DIR}.

  \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret
  tagged Isabelle command regions.  Tags are specified as a comma
  separated list of modifier/name pairs: ``@{verbatim "+"}@{text
  foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim
  "-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to
  fold text tagged as @{text foo}.  The builtin default is equivalent
  to the tag specification ``@{verbatim
  "+theory,+proof,+ML,+visible,-invisible"}''; see also the {\LaTeX}
  macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and
  @{verbatim "\\isafoldtag"}, in @{file
  "~~/lib/texinputs/isabelle.sty"}.

  \medskip Document preparation requires a @{verbatim document}
  directory within the session sources.  This directory is supposed to
  contain all the files needed to produce the final document --- apart
  from the actual theories which are generated by Isabelle.

  \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
  the same directory).

  In more complex situations, a separate @{verbatim build} script for
  the document sources may be given.  It is invoked with command-line
  arguments for the document format and the document variant name.
  The script needs to produce corresponding output files, e.g.\
  @{verbatim root.pdf} for target format @{verbatim pdf} (and default
  variants).  The main work can be again delegated to @{tool latex},
  but it is also possible to harvest generated {\LaTeX} sources and
  copy them elsewhere.

  \medskip When running the session, Isabelle copies the content of
  the original @{verbatim document} directory into its proper place
  within @{setting ISABELLE_BROWSER_INFO}, according to the session
  path and document variant.  Then, for any processed theory @{text A}
  some {\LaTeX} source is generated and put there as @{text
  A}@{verbatim ".tex"}.  Furthermore, a list of all generated theory
  files is put into @{verbatim session.tex}.  Typically, the root
  {\LaTeX} file provided by the user would include @{verbatim
  session.tex} to get a document containing all the theories.

  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 @{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
  "isabellesym.sty"} should be included as well.  This package
  contains a standard set of {\LaTeX} macro definitions @{verbatim
  "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim
  "<"}@{text foo}@{verbatim ">"}, see \cite{isabelle-implementation} for a
  complete list of predefined Isabelle symbols.  Users may invent
  further symbols as well, just by providing {\LaTeX} macros in a
  similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of
  the Isabelle distribution.

  For proper setup of DVI and PDF documents (with hyperlinks and
  bookmarks), we recommend to include @{file
  "~~/lib/texinputs/pdfsetup.sty"} as well.

  \medskip As a final step of Isabelle document preparation, @{tool
  document}~@{verbatim "-c"} is run on the resulting copy of the
  @{verbatim document} directory.  Thus the actual output document is
  built and installed in its proper place.  The generated sources are
  deleted after successful run of {\LaTeX} and friends.

  Some care is needed if the document output location is configured
  differently, say within a directory whose content is still required
  afterwards!
*}


section {* Running {\LaTeX} within the Isabelle environment
  \label{sec:tool-latex} *}

text {* The @{tool_def latex} tool provides the basic interface for
  Isabelle document preparation.  Its usage is:
\begin{ttbox}
Usage: isabelle latex [OPTIONS] [FILE]

  Options are:
    -o FORMAT    specify output format: pdf (default), dvi,
                 bbl, idx, sty, syms

  Run LaTeX (and related tools) on FILE (default root.tex),
  producing the specified output format.
\end{ttbox}

  Appropriate {\LaTeX}-related programs are run on the input file,
  according to the given output format: @{executable latex},
  @{executable pdflatex}, @{executable dvips}, @{executable bibtex}
  (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim
  idx}).  The actual commands are determined from the settings
  environment (@{setting ISABELLE_PDFLATEX} etc.).

  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.

  The @{verbatim syms} output is for internal use; it generates lists
  of symbols that are available without loading additional {\LaTeX}
  packages.
*}


subsubsection {* Examples *}

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 getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
  isabelle latex -o pdf
\end{ttbox}
*}

end