doc-src/System/browse.tex
author wenzelm
Mon, 12 May 1997 18:26:53 +0200
changeset 3170 0b3ff84bab29
permissions -rw-r--r--
The Isabelle System Manual;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3170
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
     1
\chapter{Browsing theory graphs} \label{browse}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
     2
\index{browser|bold} 
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
     3
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
     4
The graph browser {\tt browse} is a tool for visualizing
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
     5
dependency graphs of Isabelle theories. Certain nodes of
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
     6
the graph (i.e.~theories) can be grouped together in "directories",
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
     7
whose contents may be hidden, thus enabling the user to filter out
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
     8
irrelevant information. Because it is written in Java, the browser
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
     9
can be used both as a stand-alone application and as an applet.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    10
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    11
\section{Invoking the graph browser}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    12
The browser can be invoked by the command
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    13
\begin{ttbox}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    14
isatool browse [Filename]
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    15
\end{ttbox}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    16
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    17
\section{Generating graph definition files}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    18
Before browsing a theory dependency graph, a graph definition file
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    19
has to be generated. This works quite similar to the generation
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    20
of HTML files: $\ldots$ \\
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    21
A graph definition file has the following syntax:
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    22
\begin{eqnarray*}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    23
\mbox{\it graph} & = & \{ \: \mbox{\it vertex \tt ;} \: \} ^ + \\
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    24
vertex & = & \mbox{\it vertexname} \: \mbox{\it dirname} \: [ \mbox{\tt +} ]
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    25
\: \mbox{\it path} \: [ \mbox{\tt <} | \mbox{\tt >} ] \: \{ \: \mbox{\it vertexname} \: \} ^ *
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    26
\end{eqnarray*}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    27
The meaning of the items in a vertex description is as follows:
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    28
\begin{description}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    29
\item[vertexname] The name of the vertex.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    30
\item[dirname] The name of the "directory" the vertex should be placed in.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    31
A "{\tt +}" sign after {\it dirname} indicates that the nodes in the directory
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    32
are initially visible. Directories are initially invisible by default.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    33
\item[path] The path of the corresponding theory file. This is specified
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    34
relatively to the path of the graph definition file.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    35
\item[List of successor/predecessor nodes] A "{\tt <}" sign before the list
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    36
means that successor nodes are listed, a "{\tt >}" sign means that predecessor
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    37
nodes are listed. If neither "{\tt <}" nor "{\tt >}" is found, the browser
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    38
assumes that successor nodes are listed.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    39
\end{description}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    40
All names should be put in quotation marks.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    41
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    42
\section{Using the graph browser}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    43
The browser's main window, which is shown in figure \ref{browserwindow},
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    44
consists of two subwindows: In the left subwindow, the directory tree
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    45
is displayed. The graph itself is displayed in the right subwindow.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    46
\begin{figure}[h]
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    47
\setlength{\epsfxsize}{\textwidth}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    48
\epsffile{browser_screenshot.eps}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    49
\caption{\label{browserwindow} Browser main window}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    50
\end{figure}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    51
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    52
\subsection*{The directory tree window}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    53
This section describes the usage of the directory browser and the
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    54
meaning of the different items in the browser window.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    55
\begin{itemize}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    56
\item A red arrow before a directory name indicates that the directory is
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    57
currently "folded", i.e.~the nodes in this directory
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    58
are collapsed to one single node. In the right subwindow, the names of
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    59
nodes corresponding to folded directories are enclosed in square brackets
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    60
and displayed in red colour.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    61
\item A green downward arrow before a directory name indicates that the
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    62
directory is currently "unfolded". It can be folded by clicking on the
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    63
directory name.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    64
Clicking on the name for a second time unfolds the directory again.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    65
Alternatively, a directory can also be unfolded by clicking on the
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    66
corresponding node in the right subwindow.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    67
\item Blue arrows stand before ordinary node (i.e.~theory) names. When
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    68
clicking on such a name, the graph display window focuses to the
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    69
corresponding node. Double clicking invokes a text viewer window in
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    70
which the contents of the theory file are displayed.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    71
\end{itemize}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    72
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    73
\subsection*{The graph display window}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    74
When pointing on an ordinary node, an upward and a downward arrow is shown.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    75
Initially, both of these arrows are coloured green. Clicking on the
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    76
upward or downward arrow collapses all predecessor or successor nodes,
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    77
respectively. The arrow's colour then changes to red, indicating that
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    78
the predecessor or successor nodes are currently collapsed. The node
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    79
corresponding to the collapsed nodes has the name "{\tt [....]}". To
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    80
uncollapse the nodes again, simply click on the red arrow or on the node
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    81
with the name "{\tt [....]}". Similar to the directory browser, the contents
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    82
of theory files can be displayed by double clicking on the corresponding
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    83
node. 
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    84
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    85
\subsection*{The "File" menu}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    86
Please note that, due to security restrictions, this menu is not available
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    87
in the applet version. The meaning of the menu items is as follows:
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    88
\begin{description}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    89
\item[Open$\ldots$] Open a new graph file.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    90
\item[Export to PostScript] Outputs the current graph in {\sc PostScript}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    91
format, appropriately scaled to fit on one single sheet of paper.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    92
The resulting file can be sent directly to a {\sc PostScript} capable printer.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    93
\item[Export to EPS] Outputs the current graph in Encapsulated {\sc PostScript}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    94
format. The resulting file can be included in other documents (e.g.~by using
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    95
the \LaTeX \ package "epsf").
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    96
\item[Quit] Quit the graph browser.
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    97
\end{description}
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    98
0b3ff84bab29 The Isabelle System Manual;
wenzelm
parents:
diff changeset
    99
\section{The applet version of the graph browser}