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