doc-src/System/browse.tex

fixed EqI meta rule;

\chapter{Browsing theory graphs} \label{browse}
\index{browser|bold} 

The graph browser {\tt browse} is a tool for visualizing
dependency graphs of Isabelle theories. Certain nodes of
the graph (i.e.~theories) can be grouped together in "directories",
whose contents may be hidden, thus enabling the user to filter out
irrelevant information. Because it is written in Java, the browser
can be used both as a stand-alone application and as an applet.

\section{Invoking the graph browser}
The browser can be invoked by the command
\begin{ttbox}
isatool browse [Filename]
\end{ttbox}

\section{Generating graph definition files}
Before browsing a theory dependency graph, a graph definition file
has to be generated. This works quite similar to the generation
of HTML files: $\ldots$ \\
A graph definition file has the following syntax:
\begin{eqnarray*}
\mbox{\it graph} & = & \{ \: \mbox{\it vertex \tt ;} \: \} ^ + \\
vertex & = & \mbox{\it vertexname} \: \mbox{\it dirname} \: [ \mbox{\tt +} ]
\: \mbox{\it path} \: [ \mbox{\tt <} | \mbox{\tt >} ] \: \{ \: \mbox{\it vertexname} \: \} ^ *
\end{eqnarray*}
The meaning of the items in a vertex description is as follows:
\begin{description}
\item[vertexname] The name of the vertex.
\item[dirname] The name of the "directory" the vertex should be placed in.
A "{\tt +}" sign after {\it dirname} indicates that the nodes in the directory
are initially visible. Directories are initially invisible by default.
\item[path] The path of the corresponding theory file. This is specified
relatively to the path of the graph definition file.
\item[List of successor/predecessor nodes] A "{\tt <}" sign before the list
means that successor nodes are listed, a "{\tt >}" sign means that predecessor
nodes are listed. If neither "{\tt <}" nor "{\tt >}" is found, the browser
assumes that successor nodes are listed.
\end{description}
All names should be put in quotation marks.

\section{Using the graph browser}
The browser's main window, which is shown in figure \ref{browserwindow},
consists of two subwindows: In the left subwindow, the directory tree
is displayed. The graph itself is displayed in the right subwindow.
\begin{figure}[h]
\setlength{\epsfxsize}{\textwidth}
\epsffile{browser_screenshot.eps}
\caption{\label{browserwindow} Browser main window}
\end{figure}

\subsection*{The directory tree window}
This section describes the usage of the directory browser and the
meaning of the different items in the browser window.
\begin{itemize}
\item A red arrow before a directory name indicates that the directory is
currently "folded", i.e.~the nodes in this directory
are collapsed to one single node. In the right subwindow, the names of
nodes corresponding to folded directories are enclosed in square brackets
and displayed in red colour.
\item A green downward arrow before a directory name indicates that the
directory is currently "unfolded". It can be folded by clicking on the
directory name.
Clicking on the name for a second time unfolds the directory again.
Alternatively, a directory can also be unfolded by clicking on the
corresponding node in the right subwindow.
\item Blue arrows stand before ordinary node (i.e.~theory) names. When
clicking on such a name, the graph display window focuses to the
corresponding node. Double clicking invokes a text viewer window in
which the contents of the theory file are displayed.
\end{itemize}

\subsection*{The graph display window}
When pointing on an ordinary node, an upward and a downward arrow is shown.
Initially, both of these arrows are coloured green. Clicking on the
upward or downward arrow collapses all predecessor or successor nodes,
respectively. The arrow's colour then changes to red, indicating that
the predecessor or successor nodes are currently collapsed. The node
corresponding to the collapsed nodes has the name "{\tt [....]}". To
uncollapse the nodes again, simply click on the red arrow or on the node
with the name "{\tt [....]}". Similar to the directory browser, the contents
of theory files can be displayed by double clicking on the corresponding
node. 

\subsection*{The "File" menu}
Please note that, due to security restrictions, this menu is not available
in the applet version. The meaning of the menu items is as follows:
\begin{description}
\item[Open$\ldots$] Open a new graph file.
\item[Export to PostScript] Outputs the current graph in {\sc PostScript}
format, appropriately scaled to fit on one single sheet of paper.
The resulting file can be sent directly to a {\sc PostScript} capable printer.
\item[Export to EPS] Outputs the current graph in Encapsulated {\sc PostScript}
format. The resulting file can be included in other documents (e.g.~by using
the \LaTeX \ package "epsf").
\item[Quit] Quit the graph browser.
\end{description}

\section{The applet version of the graph browser}