doc-src/System/present.tex
author wenzelm
Wed, 25 Aug 1999 20:49:02 +0200
changeset 7357 d0e16da40ea2
parent 7258 b228e54a02c5
child 7849 29a2a1d71128
permissions -rw-r--r--
proper bootstrap of HOL theory and packages;
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
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
     6
\section{Generating theory browsing information} \label{sec:info}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
     7
\index{theory browsing information|bold}
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     8
7258
wenzelm
parents: 7251
diff changeset
     9
Isabelle is able to generate theory browsing information, including HTML
wenzelm
parents: 7251
diff changeset
    10
documents that show a theory's definition, the theorems proved in its ML file
wenzelm
parents: 7251
diff changeset
    11
and the relationship with its ancestors and descendants.  Besides the HTML
wenzelm
parents: 7251
diff changeset
    12
file that is generated for every theory, Isabelle stores links to all theories
wenzelm
parents: 7251
diff changeset
    13
in an index file. These indexes are linked with other indexes to represent the
wenzelm
parents: 7251
diff changeset
    14
hierarchic structure of Isabelle's logics.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    15
7258
wenzelm
parents: 7251
diff changeset
    16
Isabelle also generates graph files that represent the theory hierarchy of a
wenzelm
parents: 7251
diff changeset
    17
logic.  There is a graph browser Java applet embedded in the generated HTML
wenzelm
parents: 7251
diff changeset
    18
pages, and also a stand-alone application that allows browsing theory graphs
wenzelm
parents: 7251
diff changeset
    19
without having to start a WWW browser first.  The latter version also includes
wenzelm
parents: 7251
diff changeset
    20
features such as generating {\sc PostScript} files, which are not available in
wenzelm
parents: 7251
diff changeset
    21
the applet version.  See \S\ref{sec:browse} for further information.
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    22
7258
wenzelm
parents: 7251
diff changeset
    23
\medskip
wenzelm
parents: 7251
diff changeset
    24
wenzelm
parents: 7251
diff changeset
    25
To generate theory browsing information for logics that are part of the
wenzelm
parents: 7251
diff changeset
    26
Isabelle distribution, simply append ``\texttt{-i true}'' to the
wenzelm
parents: 7251
diff changeset
    27
\settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic.  For example,
wenzelm
parents: 7251
diff changeset
    28
in order to do this for {\FOL}, first add something like this to your Isabelle
wenzelm
parents: 7251
diff changeset
    29
settings file
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    30
\begin{ttbox}
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    31
ISABELLE_USEDIR_OPTIONS="-i true"
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    32
\end{ttbox}
7258
wenzelm
parents: 7251
diff changeset
    33
and then change into the \texttt{src/FOL} directory of the Isabelle
wenzelm
parents: 7251
diff changeset
    34
distribution and run \texttt{isatool make}, or even \texttt{isatool make all}.
wenzelm
parents: 7251
diff changeset
    35
wenzelm
parents: 7251
diff changeset
    36
\medskip
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    37
7258
wenzelm
parents: 7251
diff changeset
    38
The theory browsing information is stored within the directory determined by
wenzelm
parents: 7251
diff changeset
    39
the \settdx{ISABELLE_BROWSER_INFO} setting.  The \texttt{index.html} file
wenzelm
parents: 7251
diff changeset
    40
located there provides an entry point to all standard Isabelle logics.  A
wenzelm
parents: 7251
diff changeset
    41
complete HTML version of all object-logics and examples of the Isabelle
wenzelm
parents: 7251
diff changeset
    42
distribution is available at
6623
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    43
\begin{center}\small
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    44
  \begin{tabular}{l}
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    45
    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    46
    \url{http://isabelle.in.tum.de/library/} \\
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    47
  \end{tabular}
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    48
\end{center}
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
    49
7258
wenzelm
parents: 7251
diff changeset
    50
\medskip
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    51
7258
wenzelm
parents: 7251
diff changeset
    52
The generated HTML document of any theory includes all theorems proved in the
wenzelm
parents: 7251
diff changeset
    53
corresponding {\ML} file, provided these have been stored properly via
wenzelm
parents: 7251
diff changeset
    54
\ttindex{qed}, \ttindex{qed_goal}, \ttindex{qed_goalw}, \ttindex{bind_thm}, or
wenzelm
parents: 7251
diff changeset
    55
\ttindex{store_thm}.  Section headings may be included in the presentation via
wenzelm
parents: 7251
diff changeset
    56
the {\ML} function
wenzelm
parents: 7251
diff changeset
    57
\begin{ttbox}\index{*section}
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    58
section: string -> unit
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    59
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    60
7258
wenzelm
parents: 7251
diff changeset
    61
\medskip
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    62
7258
wenzelm
parents: 7251
diff changeset
    63
In order to present your own theories on the web, simply copy the whole
wenzelm
parents: 7251
diff changeset
    64
\texttt{ISABELLE_BROWSER_INFO} directory to your WWW server, after generating
wenzelm
parents: 7251
diff changeset
    65
browser info like this:
7251
35de2117b5dd Modified section about generation of theory browsing information.
berghofe
parents: 6623
diff changeset
    66
\begin{ttbox}
7258
wenzelm
parents: 7251
diff changeset
    67
isatool usedir -i true HOL Foobar
7251
35de2117b5dd Modified section about generation of theory browsing information.
berghofe
parents: 6623
diff changeset
    68
\end{ttbox}
7258
wenzelm
parents: 7251
diff changeset
    69
This assumes that directory \texttt{Foobar} contains some \texttt{ROOT.ML}
wenzelm
parents: 7251
diff changeset
    70
file to load all your theories, and {\HOL} is your parent logic image.
wenzelm
parents: 7251
diff changeset
    71
Ideally, theory browser information would have been generated for {\HOL}
wenzelm
parents: 7251
diff changeset
    72
already.
wenzelm
parents: 7251
diff changeset
    73
wenzelm
parents: 7251
diff changeset
    74
Alternatively, one may specify an external link to an existing body of HTML
wenzelm
parents: 7251
diff changeset
    75
data by giving \texttt{usedir} a \texttt{-P} option like this:
wenzelm
parents: 7251
diff changeset
    76
\begin{ttbox}
wenzelm
parents: 7251
diff changeset
    77
isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foobar
wenzelm
parents: 7251
diff changeset
    78
\end{ttbox}
wenzelm
parents: 7251
diff changeset
    79
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    80
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    81
\section{Browsing theory graphs} \label{sec:browse}
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    82
\index{theory graph browser|bold} 
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    83
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    84
The graph browser is a tool for visualizing dependency graphs of
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    85
Isabelle theories. Certain nodes of the graph (i.e.~theories) can be
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    86
grouped together in ``directories'', whose contents may be hidden,
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    87
thus enabling the user to filter out irrelevant information.  The
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    88
browser is written in Java, it can be used both as a stand-alone
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    89
application and as an applet.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    90
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    91
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    92
\subsection{Invoking the graph browser}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    93
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    94
The stand-alone version of the graph browser is wrapped up as an
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    95
Isabelle tool called \tooldx{browser}:
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    96
\begin{ttbox}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    97
Usage: browser [GRAPHFILE]
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    98
\end{ttbox}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    99
When no filename is specified, the browser automatically changes to
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   100
the directory \texttt{ISABELLE_BROWSER_INFO/graph/data}.
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   101
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   102
\medskip The applet version of the browser can be invoked by opening
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   103
the {\tt index.html} file in the directory
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   104
\texttt{ISABELLE_BROWSER_INFO} from your Web browser and selecting
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   105
``version for Java capable browsers''.  There is also a link to the
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   106
corresponding theory graph in every logic's {\tt index.html} file.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   107
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   108
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   109
\subsection{Using the graph browser}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   110
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   111
The browser's main window, which is shown in figure
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   112
\ref{browserwindow}, consists of two subwindows: In the left
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   113
subwindow, the directory tree is displayed. The graph itself is
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   114
displayed in the right subwindow.
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   115
\begin{figure}[h]
6623
021728c71030 pdf setup;
wenzelm
parents: 6148
diff changeset
   116
  \includegraphics[width=\textwidth]{browser_screenshot}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   117
  \caption{\label{browserwindow} Browser main window}
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   118
\end{figure}
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   119
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   120
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   121
\subsubsection*{The directory tree window}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   122
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   123
This section describes the usage of the directory browser and the
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   124
meaning of the different items in the browser window.
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   125
\begin{itemize}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   126
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   127
\item A red arrow before a directory name indicates that the directory
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   128
  is currently ``folded'', i.e.~the nodes in this directory are
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   129
  collapsed to one single node. In the right subwindow, the names of
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   130
  nodes corresponding to folded directories are enclosed in square
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   131
  brackets and displayed in red colour.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   132
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   133
\item A green downward arrow before a directory name indicates that
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   134
  the directory is currently ``unfolded''. It can be folded by
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   135
  clicking on the directory name.  Clicking on the name for a second
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   136
  time unfolds the directory again.  Alternatively, a directory can
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   137
  also be unfolded by clicking on the corresponding node in the right
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   138
  subwindow.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   139
  
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   140
\item Blue arrows stand before ordinary node (i.e.~theory) names. When
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   141
  clicking on such a name, the graph display window focuses to the
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   142
  corresponding node. Double clicking invokes a text viewer window in
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   143
  which the contents of the theory file are displayed.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   144
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   145
\end{itemize}
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   146
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   147
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   148
\subsubsection*{The graph display window}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   149
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   150
When pointing on an ordinary node, an upward and a downward arrow is
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   151
shown.  Initially, both of these arrows are green. Clicking on the
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   152
upward or downward arrow collapses all predecessor or successor nodes,
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   153
respectively. The arrow's colour then changes to red, indicating that
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   154
the predecessor or successor nodes are currently collapsed. The node
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   155
corresponding to the collapsed nodes has the name ``{\tt [....]}''. To
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   156
uncollapse the nodes again, simply click on the red arrow or on the
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   157
node with the name ``{\tt [....]}''. Similar to the directory browser,
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   158
the contents of theory files can be displayed by double clicking on
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   159
the corresponding node.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   160
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   161
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   162
\subsubsection*{The ``File'' menu}
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   163
4555
wenzelm
parents: 4540
diff changeset
   164
Please note that due to Java security restrictions this menu is not
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   165
available in the applet version. The meaning of the menu items is as
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   166
follows:
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   167
\begin{description}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   168
  
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   169
\item[Open$\ldots$] Open a new graph file.
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   170
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   171
\item[Export to PostScript] Outputs the current graph in {\sc
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   172
    PostScript} format, appropriately scaled to fit on one single
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   173
  sheet of paper.  The resulting file can printed directly.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   174
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   175
\item[Export to EPS] Outputs the current graph in Encapsulated {\sc
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   176
    PostScript} format. The resulting file can be included in other
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   177
  documents.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   178
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   179
\item[Quit] Quit the graph browser.
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   180
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   181
\end{description}
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   182
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   183
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   184
\subsection*{*Syntax of graph definition files}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   185
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   186
A graph definition file has the following syntax:
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   187
\begin{eqnarray*}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   188
  \mbox{\it graph} & = & \{ \: \mbox{\it vertex \tt ;} \: \} ^ + \\
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   189
  vertex & = & \mbox{\it vertexname} \: \mbox{\it vertexID} \: \mbox{\it dirname} \: [ \mbox{\tt +} ]
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   190
  \: \mbox{\it path} \: [ \mbox{\tt <} | \mbox{\tt >} ] \: \{ \: \mbox{\it vertexID} \: \} ^ *
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   191
\end{eqnarray*}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   192
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   193
The meaning of the items in a vertex description is as follows:
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   194
\begin{description}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   195
  
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   196
\item[vertexname] The name of the vertex.
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   197
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   198
\item[vertexID] The vertex identifier. Note that there may be two
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   199
  vertices with equal names, whereas identifiers must be unique.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   200
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   201
\item[dirname] The name of the ``directory'' the vertex should be
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   202
  placed in.  A ``{\tt +}'' sign after {\it dirname} indicates that
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   203
  the nodes in the directory are initially visible. Directories are
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   204
  initially invisible by default.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   205
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   206
\item[path] The path of the corresponding theory file. This is
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   207
  specified relatively to the path of the graph definition file.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   208
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   209
\item[List of successor/predecessor nodes] A ``{\tt <}'' sign before
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   210
  the list means that successor nodes are listed, a ``{\tt >}'' sign
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   211
  means that predecessor nodes are listed. If neither ``{\tt <}'' nor
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   212
  ``{\tt >}'' is found, the browser assumes that successor nodes are
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   213
  listed.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   214
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   215
\end{description}
5364
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   216
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   217
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   218
%%% Local Variables: 
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   219
%%% mode: latex
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   220
%%% TeX-master: "system"
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   221
%%% End: