doc-src/System/Thy/Presentation.thy
author wenzelm
Mon Sep 15 19:42:22 2008 +0200 (2008-09-15 ago)
changeset 28221 ca9fdab0f971
child 28225 5d1fc22bccdf
permissions -rw-r--r--
converted present.tex;
wenzelm@28221
     1
(* $Id$ *)
wenzelm@28221
     2
wenzelm@28221
     3
theory Presentation
wenzelm@28221
     4
imports Pure
wenzelm@28221
     5
begin
wenzelm@28221
     6
wenzelm@28221
     7
chapter {* Presenting theories \label{ch:present} *}
wenzelm@28221
     8
wenzelm@28221
     9
text {*
wenzelm@28221
    10
  Isabelle provides several ways to present the outcome of formal
wenzelm@28221
    11
  developments, including WWW-based browsable libraries or actual
wenzelm@28221
    12
  printable documents.  Presentation is centered around the concept of
wenzelm@28221
    13
  \emph{logic sessions}.  The global session structure is that of a
wenzelm@28221
    14
  tree, with Isabelle Pure at its root, further object-logics derived
wenzelm@28221
    15
  (e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions
wenzelm@28221
    16
  in leaf positions (usually without a separate image).
wenzelm@28221
    17
wenzelm@28221
    18
  The Isabelle tools @{tool_ref mkdir} and @{tool_ref make} provide
wenzelm@28221
    19
  the primary means for managing Isabelle sessions, including proper
wenzelm@28221
    20
  setup for presentation.  Here the @{tool_ref usedir} tool takes care
wenzelm@28221
    21
  to let @{executable_ref "isabelle-process"} process run any
wenzelm@28221
    22
  additional stages required for document preparation, notably the
wenzelm@28221
    23
  tools @{tool_ref document} and @{tool_ref latex}.  The complete tool
wenzelm@28221
    24
  chain for managing batch-mode Isabelle sessions is illustrated in
wenzelm@28221
    25
  \figref{fig:session-tools}.
wenzelm@28221
    26
wenzelm@28221
    27
  \begin{figure}[htbp]
wenzelm@28221
    28
  \begin{center}
wenzelm@28221
    29
  \begin{tabular}{lp{0.6\textwidth}}
wenzelm@28221
    30
wenzelm@28221
    31
      @{verbatim "isatool mkdir"} & invoked once by the user to create
wenzelm@28221
    32
      the initial source setup (common @{verbatim IsaMakefile} plus a
wenzelm@28221
    33
      single session directory); \\
wenzelm@28221
    34
wenzelm@28221
    35
      @{verbatim "isatool make"} & invoked repeatedly by the user to
wenzelm@28221
    36
      keep session output up-to-date (HTML, documents etc.); \\
wenzelm@28221
    37
wenzelm@28221
    38
      @{verbatim "isatool usedir"} & part of the standard @{verbatim
wenzelm@28221
    39
      IsaMakefile} entry of a session; \\
wenzelm@28221
    40
wenzelm@28221
    41
      @{verbatim "isabelle-process"} & run through @{verbatim "isatool
wenzelm@28221
    42
      usedir"}; \\
wenzelm@28221
    43
wenzelm@28221
    44
      @{verbatim "isatool document"} & run by the Isabelle process if
wenzelm@28221
    45
      document preparation is enabled; \\
wenzelm@28221
    46
wenzelm@28221
    47
      @{verbatim "isatool latex"} & universal {\LaTeX} tool wrapper
wenzelm@28221
    48
      invoked multiple times by @{verbatim "isatool document"}; also
wenzelm@28221
    49
      useful for manual experiments; \\
wenzelm@28221
    50
wenzelm@28221
    51
  \end{tabular}
wenzelm@28221
    52
  \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
wenzelm@28221
    53
  \end{center}
wenzelm@28221
    54
  \end{figure}
wenzelm@28221
    55
*}
wenzelm@28221
    56
wenzelm@28221
    57
wenzelm@28221
    58
section {* Generating theory browser information \label{sec:info} *}
wenzelm@28221
    59
wenzelm@28221
    60
text {*
wenzelm@28221
    61
  \index{theory browsing information|bold}
wenzelm@28221
    62
wenzelm@28221
    63
  As a side-effect of running a logic sessions, Isabelle is able to
wenzelm@28221
    64
  generate theory browsing information, including HTML documents that
wenzelm@28221
    65
  show a theory's definition, the theorems proved in its ML file and
wenzelm@28221
    66
  the relationship with its ancestors and descendants.  Besides the
wenzelm@28221
    67
  HTML file that is generated for every theory, Isabelle stores links
wenzelm@28221
    68
  to all theories in an index file. These indexes are linked with
wenzelm@28221
    69
  other indexes to represent the overall tree structure of logic
wenzelm@28221
    70
  sessions.
wenzelm@28221
    71
wenzelm@28221
    72
  Isabelle also generates graph files that represent the theory
wenzelm@28221
    73
  hierarchy of a logic.  There is a graph browser Java applet embedded
wenzelm@28221
    74
  in the generated HTML pages, and also a stand-alone application that
wenzelm@28221
    75
  allows browsing theory graphs without having to start a WWW client
wenzelm@28221
    76
  first.  The latter version also includes features such as generating
wenzelm@28221
    77
  Postscript files, which are not available in the applet version.
wenzelm@28221
    78
  See \secref{sec:browse} for further information.
wenzelm@28221
    79
wenzelm@28221
    80
  \medskip
wenzelm@28221
    81
wenzelm@28221
    82
  The easiest way to let Isabelle generate theory browsing information
wenzelm@28221
    83
  for existing sessions is to append ``@{verbatim "-i true"}'' to the
wenzelm@28221
    84
  @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim
wenzelm@28221
    85
  "isatool make"} (or @{verbatim "./build"} in the distribution).  For
wenzelm@28221
    86
  example, add something like this to your Isabelle settings file
wenzelm@28221
    87
wenzelm@28221
    88
\begin{ttbox}
wenzelm@28221
    89
ISABELLE_USEDIR_OPTIONS="-i true"
wenzelm@28221
    90
\end{ttbox}
wenzelm@28221
    91
wenzelm@28221
    92
  and then change into the @{verbatim "src/FOL"} directory of the
wenzelm@28221
    93
  Isabelle distribution and run @{verbatim "isatool make"}, or even
wenzelm@28221
    94
  @{verbatim "isatool make all"}.  The presentation output will appear
wenzelm@28221
    95
  in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
wenzelm@28221
    96
  @{verbatim "~/isabelle/browser_info/FOL"}.  Note that option
wenzelm@28221
    97
  @{verbatim "-v true"} will make the internal runs of @{tool usedir}
wenzelm@28221
    98
  more explicit about such details.
wenzelm@28221
    99
wenzelm@28221
   100
  Many standard Isabelle sessions (such as @{verbatim "HOL/ex"}) also
wenzelm@28221
   101
  provide actual printable documents.  These are prepared
wenzelm@28221
   102
  automatically as well if enabled like this, using the @{verbatim
wenzelm@28221
   103
  "-d"} option
wenzelm@28221
   104
\begin{ttbox}
wenzelm@28221
   105
ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
wenzelm@28221
   106
\end{ttbox}
wenzelm@28221
   107
  Enabling options @{verbatim "-i"} and @{verbatim "-d"}
wenzelm@28221
   108
  simultaneausly as shown above causes an appropriate ``document''
wenzelm@28221
   109
  link to be included in the HTML index.  Documents (or raw document
wenzelm@28221
   110
  sources) may be generated independently of browser information as
wenzelm@28221
   111
  well, see \secref{sec:tool-document} for further details.
wenzelm@28221
   112
wenzelm@28221
   113
  \bigskip The theory browsing information is stored in a
wenzelm@28221
   114
  sub-directory directory determined by the @{setting_ref
wenzelm@28221
   115
  ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the
wenzelm@28221
   116
  session identifier (according to the tree structure of sub-sessions
wenzelm@28221
   117
  by default).  A complete WWW view of all standard object-logics and
wenzelm@28221
   118
  examples of the Isabelle distribution is available at the Cambridge
wenzelm@28221
   119
  or Munich Isabelle sites:
wenzelm@28221
   120
  \begin{center}\small
wenzelm@28221
   121
  \begin{tabular}{l}
wenzelm@28221
   122
    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
wenzelm@28221
   123
    \url{http://isabelle.in.tum.de/library/} \\
wenzelm@28221
   124
  \end{tabular}
wenzelm@28221
   125
  \end{center}
wenzelm@28221
   126
  
wenzelm@28221
   127
  \medskip In order to present your own theories on the web, simply
wenzelm@28221
   128
  copy the corresponding subdirectory from @{setting
wenzelm@28221
   129
  ISABELLE_BROWSER_INFO} to your WWW server, having generated browser
wenzelm@28221
   130
  info like this:
wenzelm@28221
   131
\begin{ttbox}
wenzelm@28221
   132
isatool usedir -i true HOL Foo
wenzelm@28221
   133
\end{ttbox}
wenzelm@28221
   134
wenzelm@28221
   135
  This assumes that directory @{verbatim Foo} contains some @{verbatim
wenzelm@28221
   136
  ROOT.ML} file to load all your theories, and HOL is your parent
wenzelm@28221
   137
  logic image (@{verbatim isatool}~@{tool_ref mkdir} assists in
wenzelm@28221
   138
  setting up Isabelle session directories.  Theory browser information
wenzelm@28221
   139
  for HOL should have been generated already beforehand.
wenzelm@28221
   140
  Alternatively, one may specify an external link to an existing body
wenzelm@28221
   141
  of HTML data by giving @{tool usedir} a @{verbatim "-P"} option like
wenzelm@28221
   142
  this:
wenzelm@28221
   143
\begin{ttbox}
wenzelm@28221
   144
isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
wenzelm@28221
   145
\end{ttbox}
wenzelm@28221
   146
wenzelm@28221
   147
  \medskip For production use, the @{tool usedir} tool is usually
wenzelm@28221
   148
  invoked in an appropriate @{verbatim IsaMakefile}, via the Isabelle
wenzelm@28221
   149
  @{tool make} tool.  There is a separate @{tool mkdir} tool to
wenzelm@28221
   150
  provide easy setup of all this, with only minimal manual editing
wenzelm@28221
   151
  required.
wenzelm@28221
   152
\begin{ttbox}
wenzelm@28221
   153
isatool mkdir HOL Foo && isatool make
wenzelm@28221
   154
\end{ttbox}
wenzelm@28221
   155
  See \secref{sec:tool-mkdir} for more information on preparing
wenzelm@28221
   156
  Isabelle session directories, including the setup for documents.
wenzelm@28221
   157
*}
wenzelm@28221
   158
wenzelm@28221
   159
wenzelm@28221
   160
section {* Browsing theory graphs \label{sec:browse} *}
wenzelm@28221
   161
wenzelm@28221
   162
text {*
wenzelm@28221
   163
  \index{theory graph browser|bold} 
wenzelm@28221
   164
wenzelm@28221
   165
  The Isabelle graph browser is a general tool for visualizing
wenzelm@28221
   166
  dependency graphs.  Certain nodes of the graph (i.e.~theories) can
wenzelm@28221
   167
  be grouped together in ``directories'', whose contents may be
wenzelm@28221
   168
  hidden, thus enabling the user to collapse irrelevant portions of
wenzelm@28221
   169
  information.  The browser is written in Java, it can be used both as
wenzelm@28221
   170
  a stand-alone application and as an applet.  Note that the option
wenzelm@28221
   171
  @{verbatim "-g"} of @{verbatim isatool}~@{tool_ref usedir} creates
wenzelm@28221
   172
  graph presentations in batch mode for inclusion in session
wenzelm@28221
   173
  documents.
wenzelm@28221
   174
*}
wenzelm@28221
   175
wenzelm@28221
   176
wenzelm@28221
   177
subsection {* Invoking the graph browser *}
wenzelm@28221
   178
wenzelm@28221
   179
text {*
wenzelm@28221
   180
  The stand-alone version of the graph browser is wrapped up as an
wenzelm@28221
   181
  Isabelle tool called @{tool_def browser}:
wenzelm@28221
   182
wenzelm@28221
   183
\begin{ttbox}
wenzelm@28221
   184
Usage: browser [OPTIONS] [GRAPHFILE]
wenzelm@28221
   185
wenzelm@28221
   186
  Options are:
wenzelm@28221
   187
    -c           cleanup -- remove GRAPHFILE after use
wenzelm@28221
   188
    -o FILE      output to FILE (ps, eps, pdf)
wenzelm@28221
   189
\end{ttbox}
wenzelm@28221
   190
  When no filename is specified, the browser automatically changes to
wenzelm@28221
   191
  the directory @{setting ISABELLE_BROWSER_INFO}.
wenzelm@28221
   192
wenzelm@28221
   193
  \medskip The @{verbatim "-c"} option causes the input file to be
wenzelm@28221
   194
  removed after use.
wenzelm@28221
   195
wenzelm@28221
   196
  The @{verbatim "-o"} option indicates batch-mode operation, with the
wenzelm@28221
   197
  output written to the indicated file; note that @{verbatim pdf}
wenzelm@28221
   198
  produces an @{verbatim eps} copy as well.
wenzelm@28221
   199
wenzelm@28221
   200
  \medskip The applet version of the browser is part of the standard
wenzelm@28221
   201
  WWW theory presentation, see the link ``theory dependencies'' within
wenzelm@28221
   202
  each session index.
wenzelm@28221
   203
*}
wenzelm@28221
   204
wenzelm@28221
   205
wenzelm@28221
   206
subsection {* Using the graph browser *}
wenzelm@28221
   207
wenzelm@28221
   208
text {*
wenzelm@28221
   209
  The browser's main window, which is shown in
wenzelm@28221
   210
  \figref{fig:browserwindow}, consists of two sub-windows.  In the
wenzelm@28221
   211
  left sub-window, the directory tree is displayed. The graph itself
wenzelm@28221
   212
  is displayed in the right sub-window.
wenzelm@28221
   213
wenzelm@28221
   214
  \begin{figure}[ht]
wenzelm@28221
   215
  \includegraphics[width=\textwidth]{browser_screenshot}
wenzelm@28221
   216
  \caption{\label{fig:browserwindow} Browser main window}
wenzelm@28221
   217
  \end{figure}
wenzelm@28221
   218
*}
wenzelm@28221
   219
wenzelm@28221
   220
wenzelm@28221
   221
subsubsection {* The directory tree window *}
wenzelm@28221
   222
wenzelm@28221
   223
text {*
wenzelm@28221
   224
  We describe the usage of the directory browser and the meaning of
wenzelm@28221
   225
  the different items in the browser window.
wenzelm@28221
   226
wenzelm@28221
   227
  \begin{itemize}
wenzelm@28221
   228
  
wenzelm@28221
   229
  \item A red arrow before a directory name indicates that the
wenzelm@28221
   230
  directory is currently ``folded'', i.e.~the nodes in this directory
wenzelm@28221
   231
  are collapsed to one single node. In the right sub-window, the names
wenzelm@28221
   232
  of nodes corresponding to folded directories are enclosed in square
wenzelm@28221
   233
  brackets and displayed in red color.
wenzelm@28221
   234
  
wenzelm@28221
   235
  \item A green downward arrow before a directory name indicates that
wenzelm@28221
   236
  the directory is currently ``unfolded''. It can be folded by
wenzelm@28221
   237
  clicking on the directory name.  Clicking on the name for a second
wenzelm@28221
   238
  time unfolds the directory again.  Alternatively, a directory can
wenzelm@28221
   239
  also be unfolded by clicking on the corresponding node in the right
wenzelm@28221
   240
  sub-window.
wenzelm@28221
   241
  
wenzelm@28221
   242
  \item Blue arrows stand before ordinary node names. When clicking on
wenzelm@28221
   243
  such a name (i.e.\ that of a theory), the graph display window
wenzelm@28221
   244
  focuses to the corresponding node. Double clicking invokes a text
wenzelm@28221
   245
  viewer window in which the contents of the theory file are
wenzelm@28221
   246
  displayed.
wenzelm@28221
   247
wenzelm@28221
   248
  \end{itemize}
wenzelm@28221
   249
*}
wenzelm@28221
   250
wenzelm@28221
   251
wenzelm@28221
   252
subsubsection {* The graph display window *}
wenzelm@28221
   253
wenzelm@28221
   254
text {*
wenzelm@28221
   255
  When pointing on an ordinary node, an upward and a downward arrow is
wenzelm@28221
   256
  shown.  Initially, both of these arrows are green. Clicking on the
wenzelm@28221
   257
  upward or downward arrow collapses all predecessor or successor
wenzelm@28221
   258
  nodes, respectively. The arrow's color then changes to red,
wenzelm@28221
   259
  indicating that the predecessor or successor nodes are currently
wenzelm@28221
   260
  collapsed. The node corresponding to the collapsed nodes has the
wenzelm@28221
   261
  name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply
wenzelm@28221
   262
  click on the red arrow or on the node with the name ``@{verbatim
wenzelm@28221
   263
  "[....]"}''. Similar to the directory browser, the contents of
wenzelm@28221
   264
  theory files can be displayed by double clicking on the
wenzelm@28221
   265
  corresponding node.
wenzelm@28221
   266
*}
wenzelm@28221
   267
wenzelm@28221
   268
wenzelm@28221
   269
subsubsection {* The ``File'' menu *}
wenzelm@28221
   270
wenzelm@28221
   271
text {*
wenzelm@28221
   272
  Due to Java Applet security restrictions this menu is only available
wenzelm@28221
   273
  in the full application version. The meaning of the menu items is as
wenzelm@28221
   274
  follows:
wenzelm@28221
   275
wenzelm@28221
   276
  \begin{description}
wenzelm@28221
   277
  
wenzelm@28221
   278
  \item[Open \dots] Open a new graph file.
wenzelm@28221
   279
  
wenzelm@28221
   280
  \item[Export to PostScript] Outputs the current graph in Postscript
wenzelm@28221
   281
  format, appropriately scaled to fit on one single sheet of A4 paper.
wenzelm@28221
   282
  The resulting file can be printed directly.
wenzelm@28221
   283
  
wenzelm@28221
   284
  \item[Export to EPS] Outputs the current graph in Encapsulated
wenzelm@28221
   285
  Postscript format. The resulting file can be included in other
wenzelm@28221
   286
  documents.
wenzelm@28221
   287
wenzelm@28221
   288
  \item[Quit] Quit the graph browser.
wenzelm@28221
   289
wenzelm@28221
   290
  \end{description}
wenzelm@28221
   291
*}
wenzelm@28221
   292
wenzelm@28221
   293
wenzelm@28221
   294
subsection {* Syntax of graph definition files *}
wenzelm@28221
   295
wenzelm@28221
   296
text {*
wenzelm@28221
   297
  A graph definition file has the following syntax:
wenzelm@28221
   298
wenzelm@28221
   299
  \begin{tabular}{rcl}
wenzelm@28221
   300
    @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\
wenzelm@28221
   301
    @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"}
wenzelm@28221
   302
  \end{tabular}
wenzelm@28221
   303
wenzelm@28221
   304
  The meaning of the items in a vertex description is as follows:
wenzelm@28221
   305
wenzelm@28221
   306
  \begin{description}
wenzelm@28221
   307
  
wenzelm@28221
   308
  \item[@{text vertex_name}] The name of the vertex.
wenzelm@28221
   309
  
wenzelm@28221
   310
  \item[@{text vertex_ID}] The vertex identifier. Note that there may
wenzelm@28221
   311
  be several vertices with equal names, whereas identifiers must be
wenzelm@28221
   312
  unique.
wenzelm@28221
   313
  
wenzelm@28221
   314
  \item[@{text dir_name}] The name of the ``directory'' the vertex
wenzelm@28221
   315
  should be placed in.  A ``@{verbatim "+"}'' sign after @{text
wenzelm@28221
   316
  dir_name} indicates that the nodes in the directory are initially
wenzelm@28221
   317
  visible. Directories are initially invisible by default.
wenzelm@28221
   318
  
wenzelm@28221
   319
  \item[@{text path}] The path of the corresponding theory file. This
wenzelm@28221
   320
  is specified relatively to the path of the graph definition file.
wenzelm@28221
   321
  
wenzelm@28221
   322
  \item[List of successor/predecessor nodes] A ``@{verbatim "<"}''
wenzelm@28221
   323
  sign before the list means that successor nodes are listed, a
wenzelm@28221
   324
  ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If
wenzelm@28221
   325
  neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the
wenzelm@28221
   326
  browser assumes that successor nodes are listed.
wenzelm@28221
   327
wenzelm@28221
   328
  \end{description}
wenzelm@28221
   329
*}
wenzelm@28221
   330
wenzelm@28221
   331
wenzelm@28221
   332
section {* Creating Isabelle session directories
wenzelm@28221
   333
  \label{sec:tool-mkdir} *}
wenzelm@28221
   334
wenzelm@28221
   335
text {*
wenzelm@28221
   336
  The @{tool_def mkdir} utility prepares Isabelle session source
wenzelm@28221
   337
  directories, including a sensible default setup of @{verbatim
wenzelm@28221
   338
  IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document}
wenzelm@28221
   339
  directory with a minimal @{verbatim root.tex} that is sufficient to
wenzelm@28221
   340
  print all theories of the session (in the order of appearance); see
wenzelm@28221
   341
  \secref{sec:tool-document} for further information on Isabelle
wenzelm@28221
   342
  document preparation.  The usage of @{verbatim "isatool mkdir"} is:
wenzelm@28221
   343
wenzelm@28221
   344
\begin{ttbox}
wenzelm@28221
   345
Usage: mkdir [OPTIONS] [LOGIC] NAME
wenzelm@28221
   346
wenzelm@28221
   347
  Options are:
wenzelm@28221
   348
    -I FILE      alternative IsaMakefile output
wenzelm@28221
   349
    -P           include parent logic target
wenzelm@28221
   350
    -b           setup build mode (session outputs heap image)
wenzelm@28221
   351
    -q           quiet mode
wenzelm@28221
   352
wenzelm@28221
   353
  Prepare session directory, including IsaMakefile and document source,
wenzelm@28221
   354
  with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
wenzelm@28221
   355
\end{ttbox}
wenzelm@28221
   356
wenzelm@28221
   357
  The @{tool mkdir} tool is conservative in the sense that any
wenzelm@28221
   358
  existing @{verbatim IsaMakefile} etc.\ is left unchanged.  Thus it
wenzelm@28221
   359
  is safe to invoke it multiple times, although later runs may not
wenzelm@28221
   360
  have the desired effect.
wenzelm@28221
   361
wenzelm@28221
   362
  Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile}
wenzelm@28221
   363
  incrementally --- manual changes are required for multiple
wenzelm@28221
   364
  sub-sessions.  On order to get an initial working session, the only
wenzelm@28221
   365
  editing needed is to add appropriate @{ML use_thy} calls to the
wenzelm@28221
   366
  generated @{verbatim ROOT.ML} file.
wenzelm@28221
   367
*}
wenzelm@28221
   368
wenzelm@28221
   369
wenzelm@28221
   370
subsubsection {* Options *}
wenzelm@28221
   371
wenzelm@28221
   372
text {*
wenzelm@28221
   373
  The @{verbatim "-I"} option specifies an alternative to @{verbatim
wenzelm@28221
   374
  IsaMakefile} for dependencies.  Note that ``@{verbatim "-"}'' refers
wenzelm@28221
   375
  to \emph{stdout}, i.e.\ ``@{verbatim "-I-"}'' provides an easy way
wenzelm@28221
   376
  to peek at @{tool mkdir}'s idea of @{tool make} setup required for
wenzelm@28221
   377
  some particular of Isabelle session.
wenzelm@28221
   378
wenzelm@28221
   379
  \medskip The @{verbatim "-P"} option includes a target for the
wenzelm@28221
   380
  parent @{verbatim LOGIC} session in the generated @{verbatim
wenzelm@28221
   381
  IsaMakefile}.  The corresponding sources are assumed to be located
wenzelm@28221
   382
  within the Isabelle distribution.
wenzelm@28221
   383
wenzelm@28221
   384
  \medskip The @{verbatim "-b"} option sets up the current directory
wenzelm@28221
   385
  as the base for a new session that provides an actual logic image,
wenzelm@28221
   386
  as opposed to one that only runs several theories based on an
wenzelm@28221
   387
  existing image.  Note that in the latter case, everything except
wenzelm@28221
   388
  @{verbatim IsaMakefile} would be placed into a separate directory
wenzelm@28221
   389
  @{verbatim NAME}, rather than the current one.  See
wenzelm@28221
   390
  \secref{sec:tool-usedir} for further information on \emph{build
wenzelm@28221
   391
  mode} vs.\ \emph{example mode} of the @{tool usedir} utility.
wenzelm@28221
   392
wenzelm@28221
   393
  \medskip The @{verbatim "-q"} option enables quiet mode, suppressing
wenzelm@28221
   394
  further notes on how to proceed.
wenzelm@28221
   395
*}
wenzelm@28221
   396
wenzelm@28221
   397
wenzelm@28221
   398
subsubsection {* Examples *}
wenzelm@28221
   399
wenzelm@28221
   400
text {*
wenzelm@28221
   401
  The standard setup of a single ``example session'' based on the
wenzelm@28221
   402
  default logic, with proper document generation is generated like
wenzelm@28221
   403
  this:
wenzelm@28221
   404
\begin{ttbox}
wenzelm@28221
   405
isatool mkdir Foo && isatool make
wenzelm@28221
   406
\end{ttbox}
wenzelm@28221
   407
wenzelm@28221
   408
  \noindent The theory sources should be put into the @{verbatim Foo}
wenzelm@28221
   409
  directory, and its @{verbatim ROOT.ML} should be edited to load all
wenzelm@28221
   410
  required theories.  Invoking @{verbatim "isatool make"} again would
wenzelm@28221
   411
  run the whole session, generating browser information and the
wenzelm@28221
   412
  document automatically.  The @{verbatim IsaMakefile} is typically
wenzelm@28221
   413
  tuned manually later, e.g.\ adding source dependencies, or changing
wenzelm@28221
   414
  the options passed to @{tool usedir}.
wenzelm@28221
   415
wenzelm@28221
   416
  \medskip Large projects may demand further sessions, potentially
wenzelm@28221
   417
  with separate logic images being created.  This usually requires
wenzelm@28221
   418
  manual editing of the generated @{verbatim IsaMakefile}, which is
wenzelm@28221
   419
  meant to cover all of the sub-session directories at the same time
wenzelm@28221
   420
  (this is the deeper reasong why @{verbatim IsaMakefile} is not made
wenzelm@28221
   421
  part of the initial session directory created by @{verbatim "isatool
wenzelm@28221
   422
  mkdir"}).  See @{verbatim "src/HOL/IsaMakefile"} of the Isabelle
wenzelm@28221
   423
  distribution for a full-blown example.
wenzelm@28221
   424
*}
wenzelm@28221
   425
wenzelm@28221
   426
wenzelm@28221
   427
section {* Running Isabelle sessions \label{sec:tool-usedir} *}
wenzelm@28221
   428
wenzelm@28221
   429
text {*
wenzelm@28221
   430
  The @{tool_def usedir} utility builds object-logic images, or runs
wenzelm@28221
   431
  example sessions based on existing logics. Its usage is:
wenzelm@28221
   432
\begin{ttbox}
wenzelm@28221
   433
wenzelm@28221
   434
Usage: usedir [OPTIONS] LOGIC NAME
wenzelm@28221
   435
wenzelm@28221
   436
  Options are:
wenzelm@28221
   437
    -C BOOL      copy existing document directory to -D PATH (default true)
wenzelm@28221
   438
    -D PATH      dump generated document sources into PATH
wenzelm@28221
   439
    -M MAX       multithreading: maximum number of worker threads (default 1)
wenzelm@28221
   440
    -P PATH      set path for remote theory browsing information
wenzelm@28221
   441
    -T LEVEL     multithreading: trace level (default 0)
wenzelm@28221
   442
    -V VERSION   declare alternative document VERSION
wenzelm@28221
   443
    -b           build mode (output heap image, using current dir)
wenzelm@28221
   444
    -c BOOL      tell ML system to compress output image (default true)
wenzelm@28221
   445
    -d FORMAT    build document as FORMAT (default false)
wenzelm@28221
   446
    -f NAME      use ML file NAME (default ROOT.ML)
wenzelm@28221
   447
    -g BOOL      generate session graph image for document (default false)
wenzelm@28221
   448
    -i BOOL      generate theory browser information (default false)
wenzelm@28221
   449
    -m MODE      add print mode for output
wenzelm@28221
   450
    -p LEVEL     set level of detail for proof objects
wenzelm@28221
   451
    -r           reset session path
wenzelm@28221
   452
    -s NAME      override session NAME
wenzelm@28221
   453
    -v BOOL      be verbose (default false)
wenzelm@28221
   454
wenzelm@28221
   455
  Build object-logic or run examples. Also creates browsing
wenzelm@28221
   456
  information (HTML etc.) according to settings.
wenzelm@28221
   457
wenzelm@28221
   458
  ISABELLE_USEDIR_OPTIONS=
wenzelm@28221
   459
  HOL_USEDIR_OPTIONS=
wenzelm@28221
   460
\end{ttbox}
wenzelm@28221
   461
wenzelm@28221
   462
  Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
wenzelm@28221
   463
  setting is implicitly prefixed to \emph{any} @{tool usedir}
wenzelm@28221
   464
  call. Since the @{verbatim IsaMakefile}s of all object-logics
wenzelm@28221
   465
  distributed with Isabelle just invoke \texttt{usedir} for the real
wenzelm@28221
   466
  work, one may control compilation options globally via above
wenzelm@28221
   467
  variable. In particular, generation of \rmindex{HTML} browsing
wenzelm@28221
   468
  information and document preparation is controlled here.
wenzelm@28221
   469
wenzelm@28221
   470
  The @{setting_ref HOL_USEDIR_OPTIONS} setting is specific to the
wenzelm@28221
   471
  plain and main Isabelle/HOL images; its value is appended to
wenzelm@28221
   472
  @{setting ISABELLE_USEDIR_OPTIONS} for these particular sessions
wenzelm@28221
   473
  only.
wenzelm@28221
   474
*}
wenzelm@28221
   475
wenzelm@28221
   476
wenzelm@28221
   477
subsubsection {* Options *}
wenzelm@28221
   478
wenzelm@28221
   479
text {*
wenzelm@28221
   480
  Basically, there are two different modes of operation: \emph{build
wenzelm@28221
   481
  mode} (enabled through the @{verbatim "-b"} option) and
wenzelm@28221
   482
  \emph{example mode} (default).
wenzelm@28221
   483
wenzelm@28221
   484
  Calling @{tool usedir} with @{verbatim "-b"} runs @{executable
wenzelm@28221
   485
  "isabelle-process"} with input image @{verbatim LOGIC} and output to
wenzelm@28221
   486
  @{verbatim NAME}, as provided on the command line. This will be a
wenzelm@28221
   487
  batch session, running @{verbatim ROOT.ML} from the current
wenzelm@28221
   488
  directory and then quitting.  It is assumed that @{verbatim ROOT.ML}
wenzelm@28221
   489
  contains all ML commands required to build the logic.
wenzelm@28221
   490
wenzelm@28221
   491
  In example mode, @{verbatim usedir} runs a read-only session of
wenzelm@28221
   492
  @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from
wenzelm@28221
   493
  within directory @{verbatim NAME}.  It assumes that this file
wenzelm@28221
   494
  contains appropriate ML commands to run the desired examples.
wenzelm@28221
   495
wenzelm@28221
   496
  \medskip The @{verbatim "-i"} option controls theory browser data
wenzelm@28221
   497
  generation. It may be explicitly turned on or off --- as usual, the
wenzelm@28221
   498
  last occurrence of @{verbatim "-i"} on the command line wins.
wenzelm@28221
   499
wenzelm@28221
   500
  The @{verbatim "-P"} option specifies a path (or actual URL) to be
wenzelm@28221
   501
  prefixed to any \emph{non-local} reference of existing theories.
wenzelm@28221
   502
  Thus user sessions may easily link to existing Isabelle libraries
wenzelm@28221
   503
  already present on the WWW.
wenzelm@28221
   504
wenzelm@28221
   505
  The @{verbatim "-m"} options specifies additional print modes to be
wenzelm@28221
   506
  activated temporarily while the session is processed.
wenzelm@28221
   507
wenzelm@28221
   508
  \medskip The @{verbatim "-d"} option controls document preparation.
wenzelm@28221
   509
  Valid arguments are @{verbatim false} (do not prepare any document;
wenzelm@28221
   510
  this is default), or any of @{verbatim dvi}, @{verbatim dvi.gz},
wenzelm@28221
   511
  @{verbatim ps}, @{verbatim ps.gz}, @{verbatim pdf}.  The logic
wenzelm@28221
   512
  session has to provide a properly setup @{verbatim document}
wenzelm@28221
   513
  directory.  See \secref{sec:tool-document} and
wenzelm@28221
   514
  \secref{sec:tool-latex} for more details.
wenzelm@28221
   515
wenzelm@28221
   516
  \medskip The @{verbatim "-V"} option declares alternative document
wenzelm@28221
   517
  versions, consisting of name/tags pairs (cf.\ options @{verbatim
wenzelm@28221
   518
  "-n"} and @{verbatim "-t"} of the @{tool_ref document} tool).  The
wenzelm@28221
   519
  standard document is equivalent to ``@{verbatim
wenzelm@28221
   520
  "document=theory,proof,ML"}'', which means that all theory begin/end
wenzelm@28221
   521
  commands, proof body texts, and ML code will be presented
wenzelm@28221
   522
  faithfully.  An alternative version ``@{verbatim
wenzelm@28221
   523
  "outline=/proof/ML"}'' would fold proof and ML parts, replacing the
wenzelm@28221
   524
  original text by a short place-holder.  The form ``@{text
wenzelm@28221
   525
  name}@{verbatim "=-"},'' means to remove document @{text name} from
wenzelm@28221
   526
  the list of versions to be processed.  Any number of @{verbatim
wenzelm@28221
   527
  "-V"} options may be given; later declarations have precedence over
wenzelm@28221
   528
  earlier ones.
wenzelm@28221
   529
wenzelm@28221
   530
  \medskip The @{verbatim "-g"} option produces images of the theory
wenzelm@28221
   531
  dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
wenzelm@28221
   532
  generated document, both as @{verbatim session_graph.eps} and
wenzelm@28221
   533
  @{verbatim session_graph.pdf} at the same time.  To include this in
wenzelm@28221
   534
  the final {\LaTeX} document one could say @{verbatim
wenzelm@28221
   535
  "\\includegraphics{session_graph}"} in @{verbatim
wenzelm@28221
   536
  "document/root.tex"} (omitting the file-name extension enables
wenzelm@28221
   537
  {\LaTeX} to select to correct version, either for the DVI or PDF
wenzelm@28221
   538
  output path).
wenzelm@28221
   539
wenzelm@28221
   540
  \medskip The @{verbatim "-D"} option causes the generated document
wenzelm@28221
   541
  sources to be dumped at location @{verbatim PATH}; this path is
wenzelm@28221
   542
  relative to the session's main directory.  If the @{verbatim "-C"}
wenzelm@28221
   543
  option is true, this will include a copy of an existing @{verbatim
wenzelm@28221
   544
  document} directory as provided by the user.  For example,
wenzelm@28221
   545
  @{verbatim "isatool usedir -D generated HOL Foo"} produces a
wenzelm@28221
   546
  complete set of document sources at @{verbatim "Foo/generated"}.
wenzelm@28221
   547
  Subsequent invocation of @{verbatim "isatool document
wenzelm@28221
   548
  Foo/generated"} (see also \secref{sec:tool-document}) will process
wenzelm@28221
   549
  the final result independently of an Isabelle job.  This decoupled
wenzelm@28221
   550
  mode of operation facilitates debugging of serious {\LaTeX} errors,
wenzelm@28221
   551
  for example.
wenzelm@28221
   552
wenzelm@28221
   553
  \medskip The @{verbatim "-p"} option determines the level of detail
wenzelm@28221
   554
  for internal proof objects, see also the \emph{Isabelle Reference
wenzelm@28221
   555
  Manual}~\cite{isabelle-ref}.
wenzelm@28221
   556
wenzelm@28221
   557
  \medskip The @{verbatim "-v"} option causes additional information
wenzelm@28221
   558
  to be printed while running the session, notably the location of
wenzelm@28221
   559
  prepared documents.
wenzelm@28221
   560
wenzelm@28221
   561
  \medskip The @{verbatim "-M"} option specifies the maximum number of
wenzelm@28221
   562
  parallel threads used for processing independent tasks when checking
wenzelm@28221
   563
  theory sources (multithreading only works on suitable ML platforms).
wenzelm@28221
   564
  The special value of ``@{verbatim 0}'' or ``@{verbatim max}'' refers
wenzelm@28221
   565
  to the number of actual CPU cores of the underlying machine, which
wenzelm@28221
   566
  is a good starting point for optimal performance tuning.  The
wenzelm@28221
   567
  @{verbatim "-T"} option determines the level of detail in tracing
wenzelm@28221
   568
  output concerning the internal locking and scheduling in
wenzelm@28221
   569
  multithreaded operation.  This may be helpful in isolating
wenzelm@28221
   570
  performance bottle-necks, e.g.\ due to excessive wait states when
wenzelm@28221
   571
  locking critical code sections.
wenzelm@28221
   572
wenzelm@28221
   573
  \medskip Any @{tool usedir} session is named by some \emph{session
wenzelm@28221
   574
  identifier}. These accumulate, documenting the way sessions depend
wenzelm@28221
   575
  on others. For example, consider @{verbatim "Pure/FOL/ex"}, which
wenzelm@28221
   576
  refers to the examples of FOL, which in turn is built upon Pure.
wenzelm@28221
   577
wenzelm@28221
   578
  The current session's identifier is by default just the base name of
wenzelm@28221
   579
  the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim
wenzelm@28221
   580
  NAME} argument (in example mode). This may be overridden explicitly
wenzelm@28221
   581
  via the @{verbatim "-s"} option.
wenzelm@28221
   582
*}
wenzelm@28221
   583
wenzelm@28221
   584
wenzelm@28221
   585
subsubsection {* Examples *}
wenzelm@28221
   586
wenzelm@28221
   587
text {*
wenzelm@28221
   588
  Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's
wenzelm@28221
   589
  object-logics as a model for your own developments.  For example,
wenzelm@28221
   590
  see @{verbatim "src/FOL/IsaMakefile"}.  The Isabelle @{tool_ref
wenzelm@28221
   591
  mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation
wenzelm@28221
   592
  of @{tool usedir} as well.
wenzelm@28221
   593
*}
wenzelm@28221
   594
wenzelm@28221
   595
wenzelm@28221
   596
section {* Preparing Isabelle session documents
wenzelm@28221
   597
  \label{sec:tool-document} *}
wenzelm@28221
   598
wenzelm@28221
   599
text {*
wenzelm@28221
   600
  The @{tool_def document} utility prepares logic session documents,
wenzelm@28221
   601
  processing the sources both as provided by the user and generated by
wenzelm@28221
   602
  Isabelle.  Its usage is:
wenzelm@28221
   603
\begin{ttbox}
wenzelm@28221
   604
Usage: document [OPTIONS] [DIR]
wenzelm@28221
   605
wenzelm@28221
   606
  Options are:
wenzelm@28221
   607
    -c           cleanup -- be aggressive in removing old stuff
wenzelm@28221
   608
    -n NAME      specify document name (default 'document')
wenzelm@28221
   609
    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
wenzelm@28221
   610
                 ps.gz, pdf
wenzelm@28221
   611
    -t TAGS      specify tagged region markup
wenzelm@28221
   612
wenzelm@28221
   613
  Prepare the theory session document in DIR (default 'document')
wenzelm@28221
   614
  producing the specified output format.
wenzelm@28221
   615
\end{ttbox}
wenzelm@28221
   616
  This tool is usually run automatically as part of the corresponding
wenzelm@28221
   617
  Isabelle batch process, provided document preparation has been
wenzelm@28221
   618
  enabled (cf.\ the @{verbatim "-d"} option of the @{tool_ref usedir}
wenzelm@28221
   619
  tool).  It may be manually invoked on the generated browser
wenzelm@28221
   620
  information document output as well, e.g.\ in case of errors
wenzelm@28221
   621
  encountered in the batch run.
wenzelm@28221
   622
wenzelm@28221
   623
  \medskip The @{verbatim "-c"} option tells the @{tool document} tool
wenzelm@28221
   624
  to dispose the document sources after successful operation.  This is
wenzelm@28221
   625
  the right thing to do for sources generated by an Isabelle process,
wenzelm@28221
   626
  but take care of your files in manual document preparation!
wenzelm@28221
   627
wenzelm@28221
   628
  \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify
wenzelm@28221
   629
  the final output file name and format, the default is ``@{verbatim
wenzelm@28221
   630
  document.dvi}''.  Note that the result will appear in the parent of
wenzelm@28221
   631
  the target @{verbatim DIR}.
wenzelm@28221
   632
wenzelm@28221
   633
  \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret
wenzelm@28221
   634
  tagged Isabelle command regions.  Tags are specified as a comma
wenzelm@28221
   635
  separated list of modifier/name pairs: ``@{verbatim "+"}@{text
wenzelm@28221
   636
  foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim
wenzelm@28221
   637
  "-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to
wenzelm@28221
   638
  fold text tagged as @{text foo}.  The builtin default is equivalent
wenzelm@28221
   639
  to the tag specification ``@{verbatim
wenzelm@28221
   640
  "/theory,/proof,/ML,+visible,-invisible"}''; see also the {\LaTeX}
wenzelm@28221
   641
  macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and
wenzelm@28221
   642
  @{verbatim "\\isafoldtag"}, in @{verbatim isabelle.sty}.
wenzelm@28221
   643
wenzelm@28221
   644
  \medskip Document preparation requires a properly setup ``@{verbatim
wenzelm@28221
   645
  document}'' directory within the logic session sources.  This
wenzelm@28221
   646
  directory is supposed to contain all the files needed to produce the
wenzelm@28221
   647
  final document --- apart from the actual theories which are
wenzelm@28221
   648
  generated by Isabelle.
wenzelm@28221
   649
wenzelm@28221
   650
  \medskip For most practical purposes, the @{tool document} tool is
wenzelm@28221
   651
  smart enough to create any of the specified output formats, taking
wenzelm@28221
   652
  @{verbatim root.tex} supplied by the user as a starting point.  This
wenzelm@28221
   653
  even includes multiple runs of {\LaTeX} to accommodate references
wenzelm@28221
   654
  and bibliographies (the latter assumes @{verbatim root.bib} within
wenzelm@28221
   655
  the same directory).
wenzelm@28221
   656
wenzelm@28221
   657
  In more complex situations, a separate @{verbatim IsaMakefile} for
wenzelm@28221
   658
  the document sources may be given instead.  This should provide
wenzelm@28221
   659
  targets for any admissible document format; these have to produce
wenzelm@28221
   660
  corresponding output files named after @{verbatim root} as well,
wenzelm@28221
   661
  e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}.
wenzelm@28221
   662
wenzelm@28221
   663
  \medskip When running the session, Isabelle copies the original
wenzelm@28221
   664
  @{verbatim document} directory into its proper place within
wenzelm@28221
   665
  @{verbatim ISABELLE_BROWSER_INFO} according to the session path.
wenzelm@28221
   666
  Then, for any processed theory @{text A} some {\LaTeX} source is
wenzelm@28221
   667
  generated and put there as @{text A}@{verbatim ".tex"}.
wenzelm@28221
   668
  Furthermore, a list of all generated theory files is put into
wenzelm@28221
   669
  @{verbatim session.tex}.  Typically, the root {\LaTeX} file provided
wenzelm@28221
   670
  by the user would include @{verbatim session.tex} to get a document
wenzelm@28221
   671
  containing all the theories.
wenzelm@28221
   672
wenzelm@28221
   673
  The {\LaTeX} versions of the theories require some macros defined in
wenzelm@28221
   674
  @{verbatim isabelle.sty} as distributed with Isabelle.  Doing
wenzelm@28221
   675
  @{verbatim "\\usepackage{isabelle}"} in @{verbatim root.tex} should
wenzelm@28221
   676
  be fine; the underlying Isabelle @{tool latex} tool already includes
wenzelm@28221
   677
  an appropriate path specification for {\TeX} inputs.
wenzelm@28221
   678
wenzelm@28221
   679
  If the text contains any references to Isabelle symbols (such as
wenzelm@28221
   680
  @{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim
wenzelm@28221
   681
  isabellesym.sty} should be included as well.  This package contains
wenzelm@28221
   682
  a standard set of {\LaTeX} macro definitions @{verbatim
wenzelm@28221
   683
  "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim
wenzelm@28221
   684
  "<"}@{text foo}@{verbatim ">"}, (see \appref{app:symbols} for a
wenzelm@28221
   685
  complete list of predefined Isabelle symbols).  Users may invent
wenzelm@28221
   686
  further symbols as well, just by providing {\LaTeX} macros in a
wenzelm@28221
   687
  similar fashion as in @{verbatim isabellesym.sty} of the
wenzelm@28221
   688
  distribution.
wenzelm@28221
   689
wenzelm@28221
   690
  For proper setup of DVI and PDF documents (with hyperlinks and
wenzelm@28221
   691
  bookmarks), we recommend to include @{verbatim pdfsetup.sty} as
wenzelm@28221
   692
  well.
wenzelm@28221
   693
wenzelm@28221
   694
  \medskip As a final step of document preparation within Isabelle,
wenzelm@28221
   695
  @{verbatim "isatool document -c"} is run on the resulting @{verbatim
wenzelm@28221
   696
  document} directory.  Thus the actual output document is built and
wenzelm@28221
   697
  installed in its proper place (as linked by the session's @{verbatim
wenzelm@28221
   698
  index.html} if option @{verbatim "-i"} of @{tool_ref usedir} has
wenzelm@28221
   699
  been enabled, cf.\ \secref{sec:info}).  The generated sources are
wenzelm@28221
   700
  deleted after successful run of {\LaTeX} and friends.  Note that a
wenzelm@28221
   701
  separate copy of the sources may be retained by passing an option
wenzelm@28221
   702
  @{verbatim "-D"} to the @{tool usedir} utility when running the
wenzelm@28221
   703
  session.
wenzelm@28221
   704
*}
wenzelm@28221
   705
wenzelm@28221
   706
wenzelm@28221
   707
section {* Running {\LaTeX} within the Isabelle environment
wenzelm@28221
   708
  \label{sec:tool-latex} *}
wenzelm@28221
   709
wenzelm@28221
   710
text {*
wenzelm@28221
   711
  The @{tool_def latex} utility provides the basic interface for
wenzelm@28221
   712
  Isabelle document preparation.  Its usage is:
wenzelm@28221
   713
\begin{ttbox}
wenzelm@28221
   714
Usage: latex [OPTIONS] [FILE]
wenzelm@28221
   715
wenzelm@28221
   716
  Options are:
wenzelm@28221
   717
    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
wenzelm@28221
   718
                 ps.gz, pdf, bbl, idx, sty, syms
wenzelm@28221
   719
wenzelm@28221
   720
  Run LaTeX (and related tools) on FILE (default root.tex),
wenzelm@28221
   721
  producing the specified output format.
wenzelm@28221
   722
\end{ttbox}
wenzelm@28221
   723
wenzelm@28221
   724
  Appropriate {\LaTeX}-related programs are run on the input file,
wenzelm@28221
   725
  according to the given output format: @{executable latex},
wenzelm@28221
   726
  @{executable pdflatex}, @{executable dvips}, @{executable bibtex}
wenzelm@28221
   727
  (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim
wenzelm@28221
   728
  idx}).  The actual commands are determined from the settings
wenzelm@28221
   729
  environment (@{setting ISABELLE_LATEX} etc.).
wenzelm@28221
   730
wenzelm@28221
   731
  The @{verbatim sty} output format causes the Isabelle style files to
wenzelm@28221
   732
  be updated from the distribution.  This is useful in special
wenzelm@28221
   733
  situations where the document sources are to be processed another
wenzelm@28221
   734
  time by separate tools (cf.\ option @{verbatim "-D"} of the @{tool
wenzelm@28221
   735
  usedir} utility).
wenzelm@28221
   736
wenzelm@28221
   737
  The @{verbatim syms} output is for internal use; it generates lists
wenzelm@28221
   738
  of symbols that are available without loading additional {\LaTeX}
wenzelm@28221
   739
  packages.
wenzelm@28221
   740
*}
wenzelm@28221
   741
wenzelm@28221
   742
wenzelm@28221
   743
subsubsection {* Examples *}
wenzelm@28221
   744
wenzelm@28221
   745
text {*
wenzelm@28221
   746
  Invoking @{verbatim "isatool latex"} by hand may be occasionally
wenzelm@28221
   747
  useful when debugging failed attempts of the automatic document
wenzelm@28221
   748
  preparation stage of batch-mode Isabelle.  The abortive process
wenzelm@28221
   749
  leaves the sources at a certain place within @{setting
wenzelm@28221
   750
  ISABELLE_BROWSER_INFO}, see the runtime error message for details.
wenzelm@28221
   751
  This enables users to inspect {\LaTeX} runs in further detail, e.g.\
wenzelm@28221
   752
  like this:
wenzelm@28221
   753
\begin{ttbox}
wenzelm@28221
   754
  cd ~/isabelle/browser_info/HOL/Test/document
wenzelm@28221
   755
  isatool latex -o pdf
wenzelm@28221
   756
\end{ttbox}
wenzelm@28221
   757
*}
wenzelm@28221
   758
wenzelm@28221
   759
end