doc-src/System/present.tex
author wenzelm
Thu, 14 Oct 1999 12:46:30 +0200
changeset 7861 8d5d3163fd81
parent 7849 29a2a1d71128
child 7868 0cb6508f190c
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
     1
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
     2
%% $Id$
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     3
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     4
\chapter{Presenting theories}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     5
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
     6
Isabelle provides several ways to present the outcome of formal developments,
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
     7
including WWW-based browsable libraries or actual printable documents.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
     8
Presentation is centered around the concept of \emph{logic sessions}.  The
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
     9
structure of sessions is that of a tree, with Isabelle \texttt{Pure} at its
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    10
root, further derived object-logics (e.g.\ \texttt{HOLCF} from \texttt{HOL},
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    11
and \texttt{HOL} from \texttt{Pure}), and application sessions at its leaves.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    12
The latter usually do not have a separate {\ML} image.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    13
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    14
The \texttt{usedir} utility (see \S\ref{sec:tool-usedir}) provides the prime
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    15
means for managing Isabelle sessions, including proper setup for presentation.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    16
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    17
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    18
\section{Generating theory browsing information} \label{sec:info}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    19
\index{theory browsing information|bold}
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    20
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    21
As a side-effect of running a logic sessions, Isabelle is able to generate
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    22
theory browsing information, including HTML documents that show a theory's
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    23
definition, the theorems proved in its ML file and the relationship with its
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    24
ancestors and descendants.  Besides the HTML file that is generated for every
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    25
theory, Isabelle stores links to all theories in an index file. These indexes
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    26
are linked with other indexes to represent the tree structure of Isabelle's
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    27
logics.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    28
7258
wenzelm
parents: 7251
diff changeset
    29
Isabelle also generates graph files that represent the theory hierarchy of a
wenzelm
parents: 7251
diff changeset
    30
logic.  There is a graph browser Java applet embedded in the generated HTML
wenzelm
parents: 7251
diff changeset
    31
pages, and also a stand-alone application that allows browsing theory graphs
wenzelm
parents: 7251
diff changeset
    32
without having to start a WWW browser first.  The latter version also includes
wenzelm
parents: 7251
diff changeset
    33
features such as generating {\sc PostScript} files, which are not available in
wenzelm
parents: 7251
diff changeset
    34
the applet version.  See \S\ref{sec:browse} for further information.
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    35
7258
wenzelm
parents: 7251
diff changeset
    36
\medskip
wenzelm
parents: 7251
diff changeset
    37
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    38
In order to let Isabelle generate theory browsing information for logics that
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    39
are part of the Isabelle distribution, simply append ``\texttt{-i true}'' to
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    40
the \settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic.  For
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    41
example, in order to do this for {\FOL}, add something like this to your
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    42
Isabelle settings file
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    43
\begin{ttbox}
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    44
ISABELLE_USEDIR_OPTIONS="-i true"
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    45
\end{ttbox}
7258
wenzelm
parents: 7251
diff changeset
    46
and then change into the \texttt{src/FOL} directory of the Isabelle
wenzelm
parents: 7251
diff changeset
    47
distribution and run \texttt{isatool make}, or even \texttt{isatool make all}.
wenzelm
parents: 7251
diff changeset
    48
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    49
Some sessions (such as \texttt{HOL/Isar_examples}) even provide actual
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    50
printable documents.  These are prepared automatically as well if enabled by
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    51
giving an appropriate \texttt{-d} option, e.g.\
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    52
\begin{ttbox}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    53
ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    54
\end{ttbox}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    55
See \S\ref{sec:tool-document} for further information on Isabelle document
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    56
preparation.
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    57
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    58
\bigskip The theory browsing information is stored within the directory
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    59
determined by the \settdx{ISABELLE_BROWSER_INFO} setting.  The
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    60
\texttt{index.html} file located there provides an entry point to all standard
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    61
Isabelle logics.  A complete HTML version of all object-logics and examples of
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    62
the Isabelle distribution is available at
6623
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    63
\begin{center}\small
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    64
  \begin{tabular}{l}
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    65
    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    66
    \url{http://isabelle.in.tum.de/library/} \\
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    67
  \end{tabular}
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    68
\end{center}
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    69
7258
wenzelm
parents: 7251
diff changeset
    70
\medskip
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    71
7258
wenzelm
parents: 7251
diff changeset
    72
The generated HTML document of any theory includes all theorems proved in the
wenzelm
parents: 7251
diff changeset
    73
corresponding {\ML} file, provided these have been stored properly via
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    74
\ttindex{qed}, \ttindex{qed_goal}, \ttindex{qed_goalw}, \ttindex{bind_thm},
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    75
\ttindex{bind_thms} or \ttindex{store_thm}.  Section headings may be included
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
    76
in the presentation via the {\ML} function
7258
wenzelm
parents: 7251
diff changeset
    77
\begin{ttbox}\index{*section}
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    78
section: string -> unit
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    79
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    80
7258
wenzelm
parents: 7251
diff changeset
    81
\medskip
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    82
7258
wenzelm
parents: 7251
diff changeset
    83
In order to present your own theories on the web, simply copy the whole
wenzelm
parents: 7251
diff changeset
    84
\texttt{ISABELLE_BROWSER_INFO} directory to your WWW server, after generating
wenzelm
parents: 7251
diff changeset
    85
browser info like this:
7251
35de2117b5dd Modified section about generation of theory browsing information.
berghofe
parents: 6623
diff changeset
    86
\begin{ttbox}
7861
wenzelm
parents: 7849
diff changeset
    87
isatool usedir -i true HOL Foo
7251
35de2117b5dd Modified section about generation of theory browsing information.
berghofe
parents: 6623
diff changeset
    88
\end{ttbox}
7861
wenzelm
parents: 7849
diff changeset
    89
This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file
wenzelm
parents: 7849
diff changeset
    90
to load all your theories, and {\HOL} is your parent logic image.  Ideally,
wenzelm
parents: 7849
diff changeset
    91
theory browser information would have been generated for {\HOL} already.
7258
wenzelm
parents: 7251
diff changeset
    92
wenzelm
parents: 7251
diff changeset
    93
Alternatively, one may specify an external link to an existing body of HTML
wenzelm
parents: 7251
diff changeset
    94
data by giving \texttt{usedir} a \texttt{-P} option like this:
wenzelm
parents: 7251
diff changeset
    95
\begin{ttbox}
7861
wenzelm
parents: 7849
diff changeset
    96
isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
7258
wenzelm
parents: 7251
diff changeset
    97
\end{ttbox}
wenzelm
parents: 7251
diff changeset
    98
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    99
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   100
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   101
\section{Browsing theory graphs} \label{sec:browse}
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   102
\index{theory graph browser|bold} 
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   103
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   104
The graph browser is a tool for visualizing dependency graphs of
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   105
Isabelle theories. Certain nodes of the graph (i.e.~theories) can be
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   106
grouped together in ``directories'', whose contents may be hidden,
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   107
thus enabling the user to filter out irrelevant information.  The
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   108
browser is written in Java, it can be used both as a stand-alone
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   109
application and as an applet.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   110
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   111
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   112
\subsection{Invoking the graph browser}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   113
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   114
The stand-alone version of the graph browser is wrapped up as an
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   115
Isabelle tool called \tooldx{browser}:
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   116
\begin{ttbox}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   117
Usage: browser [GRAPHFILE]
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   118
\end{ttbox}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   119
When no filename is specified, the browser automatically changes to
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   120
the directory \texttt{ISABELLE_BROWSER_INFO/graph/data}.
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   121
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   122
\medskip The applet version of the browser can be invoked by opening the {\tt
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   123
  index.html} file in the directory \texttt{ISABELLE_BROWSER_INFO} from your
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   124
Web browser and selecting ``version for Java capable browsers''.  There is
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   125
also a link to the corresponding theory graph in every logic's {\tt
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   126
  index.html} file.
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   127
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   128
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   129
\subsection{Using the graph browser}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   130
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   131
The browser's main window, which is shown in figure
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   132
\ref{browserwindow}, consists of two sub-windows: In the left
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   133
sub-window, the directory tree is displayed. The graph itself is
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   134
displayed in the right sub-window.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   135
\begin{figure}[ht]
6623
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
   136
  \includegraphics[width=\textwidth]{browser_screenshot}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   137
  \caption{\label{browserwindow} Browser main window}
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   138
\end{figure}
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   139
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   140
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   141
\subsubsection*{The directory tree window}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   142
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   143
This section describes the usage of the directory browser and the
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   144
meaning of the different items in the browser window.
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   145
\begin{itemize}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   146
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   147
\item A red arrow before a directory name indicates that the directory
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   148
  is currently ``folded'', i.e.~the nodes in this directory are
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   149
  collapsed to one single node. In the right sub-window, the names of
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   150
  nodes corresponding to folded directories are enclosed in square
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   151
  brackets and displayed in red color.
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   152
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   153
\item A green downward arrow before a directory name indicates that
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   154
  the directory is currently ``unfolded''. It can be folded by
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   155
  clicking on the directory name.  Clicking on the name for a second
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   156
  time unfolds the directory again.  Alternatively, a directory can
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   157
  also be unfolded by clicking on the corresponding node in the right
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   158
  sub-window.
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   159
  
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   160
\item Blue arrows stand before ordinary node (i.e.~theory) names. When
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   161
  clicking on such a name, the graph display window focuses to the
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   162
  corresponding node. Double clicking invokes a text viewer window in
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   163
  which the contents of the theory file are displayed.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   164
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   165
\end{itemize}
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   166
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   167
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   168
\subsubsection*{The graph display window}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   169
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   170
When pointing on an ordinary node, an upward and a downward arrow is
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   171
shown.  Initially, both of these arrows are green. Clicking on the
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   172
upward or downward arrow collapses all predecessor or successor nodes,
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   173
respectively. The arrow's color then changes to red, indicating that
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   174
the predecessor or successor nodes are currently collapsed. The node
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   175
corresponding to the collapsed nodes has the name ``{\tt [....]}''. To
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   176
uncollapse the nodes again, simply click on the red arrow or on the
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   177
node with the name ``{\tt [....]}''. Similar to the directory browser,
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   178
the contents of theory files can be displayed by double clicking on
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   179
the corresponding node.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   180
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   181
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   182
\subsubsection*{The ``File'' menu}
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   183
4555
wenzelm
parents: 4540
diff changeset
   184
Please note that due to Java security restrictions this menu is not
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   185
available in the applet version. The meaning of the menu items is as
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   186
follows:
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   187
\begin{description}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   188
  
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   189
\item[Open$\ldots$] Open a new graph file.
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   190
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   191
\item[Export to PostScript] Outputs the current graph in {\sc
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   192
    PostScript} format, appropriately scaled to fit on one single
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   193
  sheet of paper.  The resulting file can printed directly.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   194
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   195
\item[Export to EPS] Outputs the current graph in Encapsulated {\sc
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   196
    PostScript} format. The resulting file can be included in other
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   197
  documents.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   198
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   199
\item[Quit] Quit the graph browser.
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   200
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   201
\end{description}
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   202
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   203
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   204
\subsection*{*Syntax of graph definition files}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   205
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   206
A graph definition file has the following syntax:
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   207
\begin{eqnarray*}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   208
  \mbox{\it graph} & = & \{ \: \mbox{\it vertex \tt ;} \: \} ^ + \\
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   209
  vertex & = & \mbox{\it vertexname} \: \mbox{\it vertexID} \: \mbox{\it dirname} \: [ \mbox{\tt +} ]
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   210
  \: \mbox{\it path} \: [ \mbox{\tt <} | \mbox{\tt >} ] \: \{ \: \mbox{\it vertexID} \: \} ^ *
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   211
\end{eqnarray*}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   212
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   213
The meaning of the items in a vertex description is as follows:
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   214
\begin{description}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   215
  
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   216
\item[vertexname] The name of the vertex.
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   217
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   218
\item[vertexID] The vertex identifier. Note that there may be two
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   219
  vertices with equal names, whereas identifiers must be unique.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   220
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   221
\item[dirname] The name of the ``directory'' the vertex should be
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   222
  placed in.  A ``{\tt +}'' sign after {\it dirname} indicates that
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   223
  the nodes in the directory are initially visible. Directories are
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   224
  initially invisible by default.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   225
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   226
\item[path] The path of the corresponding theory file. This is
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   227
  specified relatively to the path of the graph definition file.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   228
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   229
\item[List of successor/predecessor nodes] A ``{\tt <}'' sign before
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   230
  the list means that successor nodes are listed, a ``{\tt >}'' sign
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   231
  means that predecessor nodes are listed. If neither ``{\tt <}'' nor
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   232
  ``{\tt >}'' is found, the browser assumes that successor nodes are
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   233
  listed.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   234
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   235
\end{description}
5364
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   236
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   237
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   238
\section{Preparing Isabelle session documents --- \texttt{isatool document}}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   239
\label{sec:tool-document}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   240
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   241
The \tooldx{document} utility prepares logic session documents, processing the
7861
wenzelm
parents: 7849
diff changeset
   242
sources both provided by the user and generated by Isabelle.  Its usage is:
7849
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   243
\begin{ttbox}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   244
Usage: document [OPTIONS] [DIR]
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   245
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   246
  Options are:
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   247
    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   248
                 ps.gz, pdf
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   249
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   250
  Prepare the theory session document in DIR (default '.')
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   251
  producing the specified output format.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   252
\end{ttbox}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   253
This tool is usually run automatically as part of the corresponding session,
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   254
provided document preparation is enabled (cf.\ the \texttt{-d} option of the
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   255
\texttt{usedir} utility, \S\ref{sec:tool-usedir}).  It may be manually invoked
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   256
on the generated browser information document output as well.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   257
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   258
\medskip Document preparation requires a properly setup ``\texttt{document}''
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   259
directory within the logic session sources.  This directory is supposed to
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   260
contain all the files needed to produce the actual document, apart from the
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   261
actual theories as generated by Isabelle.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   262
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   263
\medskip For simple documents, the \texttt{document} tool is smart enough to
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   264
create any of the output formats, taking \texttt{root.tex} supplied by the
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   265
user as a starting point.  This even includes multiple runs of {\LaTeX} to
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   266
accommodate references and bibliographies (the latter assumes
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   267
\texttt{root.bib} within the same directory).
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   268
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   269
For complex documents, a separate \texttt{IsaMakefile} may be given instead.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   270
It should provide targets for any admissible document format; these have to
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   271
produce corresponding output files named after \texttt{root} as well, e.g.\ 
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   272
\texttt{root.dvi} for target format \texttt{dvi}.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   273
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   274
\medskip When running the session, Isabelle copies the original
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   275
\texttt{document} directory into its proper place within
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   276
\texttt{ISABELLE_BROWSER_INFO} according to the session path.  Then, for any
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   277
processed theory $A$ some {\LaTeX} source is generated and put there as
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   278
$A$\texttt{.tex}.  Furthermore, a list of all generated theory files is put
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   279
into \texttt{session.tex}.  Typically, the root {\LaTeX} file provided by the
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   280
user would include \texttt{session.tex} to get a document containing all the
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   281
theories.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   282
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   283
The {\LaTeX} versions of the theories require some macros defined in
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   284
\texttt{isabelle.sty} as distributed with Isabelle.  Doing
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   285
\verb,\usepackage{isabelle}, somewhere in \texttt{root.tex} should work fine;
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   286
the underlying Isabelle \texttt{latex} utility already includes an appropriate
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   287
{\TeX} inputs path.  For proper setup of hyperlinks and bookmarks in PDF
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   288
documents we recommend to include \verb,pdfsetup.sty, as well.\footnote{It is
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   289
  safe to do so even without using PDF~\LaTeX.}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   290
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   291
\medskip As a final step, \texttt{isatool document} is run on the resulting
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   292
\texttt{document} directory.  Thus the actual output document is built and
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   293
installed in its proper place (as linked by the session's
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   294
\texttt{index.html}).  Note that the generated sources are left as is.  While
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   295
they may be safely deleted afterwards, this is \emph{not} done automatically.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   296
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   297
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   298
\section{Running {\LaTeX} within the Isabelle environment --- \texttt{isatool latex}}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   299
\label{sec:tool-latex}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   300
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   301
The \tooldx{latex} utility provides the basic interface for Isabelle document
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   302
preparation.  Its usage is:
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   303
\begin{ttbox}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   304
Usage: latex [OPTIONS] [FILE]
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   305
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   306
  Options are:
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   307
    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   308
                 ps.gz, pdf, or bbl
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   309
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   310
  Run LaTeX (and related tools) on FILE (default root.tex),
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   311
  producing the specified output format.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   312
\end{ttbox}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   313
Appropriate {\LaTeX}-related programs are run on the input file, according to
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   314
the given output format: \texttt{latex}, \texttt{pdflatex}, \texttt{bibtex},
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   315
\texttt{dvips}.  The actual commands are determined from the settings
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   316
environment (see \texttt{ISABELLE_LATEX} etc.).
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   317
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   318
It is important to note that the {\LaTeX} inputs file space has to be properly
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   319
setup to include the Isabelle styles.  Usually, this may be done by modifying
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   320
the \settdx{TEXINPUTS} variable in settings like this:
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   321
\begin{ttbox}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   322
TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS"
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   323
\end{ttbox}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   324
This is known to work with recent versions of the \textsl{teTeX} distribution.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   325
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   326
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   327
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   328
\section{Managing logic sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   329
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   330
The \tooldx{usedir} utility builds object-logic images, or runs example
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   331
sessions based on existing logics. Its usage is:
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   332
\begin{ttbox}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   333
Usage: usedir LOGIC NAME
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   334
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   335
  Options are:
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   336
    -B           build mode with THIS_IS_ISABELLE_BUILD indication
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   337
    -P PATH      set path for remote theory browsing information
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   338
    -b           build mode (output heap image, using current dir)
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   339
    -d FORMAT    build document as FORMAT (default false)
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   340
    -i BOOL      generate theory browsing information,
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   341
                 i.e. HTML / graph data (default false)
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   342
    -r           reset session path
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   343
    -s NAME      override session NAME
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   344
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   345
  Build object-logic or run examples. Also creates browsing
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   346
  information (HTML etc.) according to settings.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   347
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   348
  ISABELLE_USEDIR_OPTIONS=
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   349
\end{ttbox}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   350
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   351
Note that the value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   352
implicitly prefixed to \emph{any} \texttt{usedir} call. Since the
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   353
\ttindex{IsaMakefile}s of all object-logics distributed with Isabelle just
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   354
invoke \texttt{usedir} for the real work, one may control compilation options
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   355
globally via above variable. In particular, generation of \rmindex{HTML}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   356
browsing information and document preparation is controlled this way.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   357
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   358
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   359
\subsection*{Options}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   360
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   361
Basically, there are two different modes of operation: \emph{build
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   362
  mode} (enabled through the \texttt{-b} option) and \emph{example
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   363
  mode} (default).
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   364
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   365
Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with input
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   366
image \texttt{LOGIC} and output to \texttt{NAME}, as provided on the command
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   367
line. This will be a batch session, running \texttt{ROOT.ML} from the current
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   368
directory and then quitting.  It is assumed that \texttt{ROOT.ML} contains all
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   369
{\ML} commands required to build the logic.  The \texttt{-B} option is like
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   370
\texttt{-b}, but also indicates \texttt{THIS_IS_ISABELLE_BUILD=true} via the
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   371
process environment.  This usually causes the \texttt{ISABELLE\_OUTPUT} and
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   372
\texttt{ISABELLE_BROWSER_INFO} settings to refer to some location within the
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   373
Isabelle distribution directory, rather than the user's home directory.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   374
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   375
In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   376
(typically just built before) and automatically runs \texttt{ROOT.ML} from
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   377
within directory \texttt{NAME}.  It assumes that file \texttt{ROOT.ML} in
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   378
directory \texttt{NAME} contains appropriate {\ML} commands to run the desired
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   379
examples.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   380
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   381
\medskip The \texttt{-i} option controls theory browsing data generation. It
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   382
may be explicitly turned on or off --- the last occurrence of \texttt{-i} on
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   383
the command line wins.  The \texttt{-P} option specifies a path (or actual
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   384
URL) to be prefixed to any \emph{non-local} reference of existing theories.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   385
Thus user sessions may easily link to existing Isabelle libraries already
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   386
present on the WWW.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   387
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   388
\medskip The \texttt{-d} option controls document preparation.  Valid
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   389
arguments are \texttt{false} (do not prepare document; this is default), or
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   390
any of \texttt{dvi}, \texttt{dvi.gz}, \texttt{ps}, \texttt{ps.gz},
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   391
\texttt{pdf}.  The logic session has to provide a properly setup
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   392
\texttt{document} directory.  See \S\ref{sec:tool-document} and
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   393
\S\ref{sec:tool-latex} for more details.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   394
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   395
\medskip Any \texttt{usedir} session is named by some \emph{session
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   396
  identifier}. These accumulate, documenting the way sessions depend
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   397
on others. For example, consider \texttt{Pure/FOL/ex}, which refers to
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   398
the examples of {\FOL} which is built upon {\Pure}.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   399
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   400
The current session's identifier is by default just the base name of
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   401
the \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   402
argument (in example mode). This may be overridden explicitely via the
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   403
\texttt{-s} option.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   404
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   405
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   406
\subsection*{Examples}
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   407
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   408
Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   409
object-logics as a model for your own developments.  For example, see
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   410
\texttt{src/FOL/IsaMakefile}.
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   411
29a2a1d71128 updated;
wenzelm
parents: 7258
diff changeset
   412
5364
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   413
%%% Local Variables: 
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   414
%%% mode: latex
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   415
%%% TeX-master: "system"
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   416
%%% End: