# HG changeset patch
# User berghofe
# Date 875633334 -7200
# Node ID 7f33a2015381657a1c3d87a233859824f7dfe768
# Parent  0e74b6b7f66fb183fbd904564b0211eb0232d55d
Theory browser stuff has been moved to "present.tex".

diff -r 0e74b6b7f66f -r 7f33a2015381 doc-src/System/browse.tex
--- a/doc-src/System/browse.tex	Tue Sep 30 16:19:27 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-\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}