--- a/doc-src/System/Thy/Interfaces.thy Sat Jul 28 13:18:34 2012 +0200
+++ b/doc-src/System/Thy/Interfaces.thy Sat Jul 28 13:29:56 2012 +0200
@@ -105,4 +105,180 @@
infrastructure itself. Invoking @{ML Isar.loop}~@{verbatim "();"}
in ML will return to the Isar toplevel. *}
+
+
+section {* Theory graph browser \label{sec:browse} *}
+
+text {* The Isabelle graph browser is a general tool for visualizing
+ dependency graphs. Certain nodes of the graph (i.e.\ theories) can
+ be grouped together in ``directories'', whose contents may be
+ hidden, thus enabling the user to collapse irrelevant portions of
+ information. The browser is written in Java, it can be used both as
+ a stand-alone application and as an applet. Note that the option
+ @{verbatim "-g"} of @{verbatim isabelle} @{tool_ref usedir} creates
+ graph presentations in batch mode for inclusion in session
+ documents. *}
+
+
+subsection {* Invoking the graph browser *}
+
+text {*
+ The stand-alone version of the graph browser is wrapped up as an
+ Isabelle tool called @{tool_def browser}:
+
+\begin{ttbox}
+Usage: browser [OPTIONS] [GRAPHFILE]
+
+ Options are:
+ -b Admin/build only
+ -c cleanup -- remove GRAPHFILE after use
+ -o FILE output to FILE (ps, eps, pdf)
+\end{ttbox}
+ When no filename is specified, the browser automatically changes to
+ the directory @{setting ISABELLE_BROWSER_INFO}.
+
+ \medskip The @{verbatim "-b"} option indicates that this is for
+ administrative build only, i.e.\ no browser popup if no files are
+ given.
+
+ The @{verbatim "-c"} option causes the input file to be removed
+ after use.
+
+ The @{verbatim "-o"} option indicates batch-mode operation, with the
+ output written to the indicated file; note that @{verbatim pdf}
+ produces an @{verbatim eps} copy as well.
+
+ \medskip The applet version of the browser is part of the standard
+ WWW theory presentation, see the link ``theory dependencies'' within
+ each session index.
+*}
+
+
+subsection {* Using the graph browser *}
+
+text {*
+ The browser's main window, which is shown in
+ \figref{fig:browserwindow}, consists of two sub-windows. In the
+ left sub-window, the directory tree is displayed. The graph itself
+ is displayed in the right sub-window.
+
+ \begin{figure}[ht]
+ \includegraphics[width=\textwidth]{browser_screenshot}
+ \caption{\label{fig:browserwindow} Browser main window}
+ \end{figure}
+*}
+
+
+subsubsection {* The directory tree window *}
+
+text {*
+ We describe 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 sub-window, the names
+ of nodes corresponding to folded directories are enclosed in square
+ brackets and displayed in red color.
+
+ \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
+ sub-window.
+
+ \item Blue arrows stand before ordinary node names. When clicking on
+ such a name (i.e.\ that of a theory), 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}
+*}
+
+
+subsubsection {* The graph display window *}
+
+text {*
+ When pointing on an ordinary node, an upward and a downward arrow is
+ shown. Initially, both of these arrows are green. Clicking on the
+ upward or downward arrow collapses all predecessor or successor
+ nodes, respectively. The arrow's color then changes to red,
+ indicating that the predecessor or successor nodes are currently
+ collapsed. The node corresponding to the collapsed nodes has the
+ name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply
+ click on the red arrow or on the node with the name ``@{verbatim
+ "[....]"}''. Similar to the directory browser, the contents of
+ theory files can be displayed by double clicking on the
+ corresponding node.
+*}
+
+
+subsubsection {* The ``File'' menu *}
+
+text {*
+ Due to Java Applet security restrictions this menu is only available
+ in the full application version. The meaning of the menu items is as
+ follows:
+
+ \begin{description}
+
+ \item[Open \dots] Open a new graph file.
+
+ \item[Export to PostScript] Outputs the current graph in Postscript
+ format, appropriately scaled to fit on one single sheet of A4 paper.
+ The resulting file can be printed directly.
+
+ \item[Export to EPS] Outputs the current graph in Encapsulated
+ Postscript format. The resulting file can be included in other
+ documents.
+
+ \item[Quit] Quit the graph browser.
+
+ \end{description}
+*}
+
+
+subsection {* Syntax of graph definition files *}
+
+text {*
+ A graph definition file has the following syntax:
+
+ \begin{center}\small
+ \begin{tabular}{rcl}
+ @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\
+ @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}
+ \end{tabular}
+ \end{center}
+
+ The meaning of the items in a vertex description is as follows:
+
+ \begin{description}
+
+ \item[@{text vertex_name}] The name of the vertex.
+
+ \item[@{text vertex_ID}] The vertex identifier. Note that there may
+ be several vertices with equal names, whereas identifiers must be
+ unique.
+
+ \item[@{text dir_name}] The name of the ``directory'' the vertex
+ should be placed in. A ``@{verbatim "+"}'' sign after @{text
+ dir_name} indicates that the nodes in the directory are initially
+ visible. Directories are initially invisible by default.
+
+ \item[@{text 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 ``@{verbatim "<"}''
+ sign before the list means that successor nodes are listed, a
+ ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If
+ neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the
+ browser assumes that successor nodes are listed.
+
+ \end{description}
+*}
+
end
\ No newline at end of file
--- a/doc-src/System/Thy/Presentation.thy Sat Jul 28 13:18:34 2012 +0200
+++ b/doc-src/System/Thy/Presentation.thy Sat Jul 28 13:29:56 2012 +0200
@@ -157,185 +157,6 @@
*}
-section {* Browsing theory graphs \label{sec:browse} *}
-
-text {*
- \index{theory graph browser|bold}
-
- The Isabelle graph browser is a general tool for visualizing
- dependency graphs. Certain nodes of the graph (i.e.~theories) can
- be grouped together in ``directories'', whose contents may be
- hidden, thus enabling the user to collapse irrelevant portions of
- information. The browser is written in Java, it can be used both as
- a stand-alone application and as an applet. Note that the option
- @{verbatim "-g"} of @{verbatim isabelle} @{tool_ref usedir} creates
- graph presentations in batch mode for inclusion in session
- documents.
-*}
-
-
-subsection {* Invoking the graph browser *}
-
-text {*
- The stand-alone version of the graph browser is wrapped up as an
- Isabelle tool called @{tool_def browser}:
-
-\begin{ttbox}
-Usage: browser [OPTIONS] [GRAPHFILE]
-
- Options are:
- -b Admin/build only
- -c cleanup -- remove GRAPHFILE after use
- -o FILE output to FILE (ps, eps, pdf)
-\end{ttbox}
- When no filename is specified, the browser automatically changes to
- the directory @{setting ISABELLE_BROWSER_INFO}.
-
- \medskip The @{verbatim "-b"} option indicates that this is for
- administrative build only, i.e.\ no browser popup if no files are
- given.
-
- The @{verbatim "-c"} option causes the input file to be removed
- after use.
-
- The @{verbatim "-o"} option indicates batch-mode operation, with the
- output written to the indicated file; note that @{verbatim pdf}
- produces an @{verbatim eps} copy as well.
-
- \medskip The applet version of the browser is part of the standard
- WWW theory presentation, see the link ``theory dependencies'' within
- each session index.
-*}
-
-
-subsection {* Using the graph browser *}
-
-text {*
- The browser's main window, which is shown in
- \figref{fig:browserwindow}, consists of two sub-windows. In the
- left sub-window, the directory tree is displayed. The graph itself
- is displayed in the right sub-window.
-
- \begin{figure}[ht]
- \includegraphics[width=\textwidth]{browser_screenshot}
- \caption{\label{fig:browserwindow} Browser main window}
- \end{figure}
-*}
-
-
-subsubsection {* The directory tree window *}
-
-text {*
- We describe 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 sub-window, the names
- of nodes corresponding to folded directories are enclosed in square
- brackets and displayed in red color.
-
- \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
- sub-window.
-
- \item Blue arrows stand before ordinary node names. When clicking on
- such a name (i.e.\ that of a theory), 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}
-*}
-
-
-subsubsection {* The graph display window *}
-
-text {*
- When pointing on an ordinary node, an upward and a downward arrow is
- shown. Initially, both of these arrows are green. Clicking on the
- upward or downward arrow collapses all predecessor or successor
- nodes, respectively. The arrow's color then changes to red,
- indicating that the predecessor or successor nodes are currently
- collapsed. The node corresponding to the collapsed nodes has the
- name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply
- click on the red arrow or on the node with the name ``@{verbatim
- "[....]"}''. Similar to the directory browser, the contents of
- theory files can be displayed by double clicking on the
- corresponding node.
-*}
-
-
-subsubsection {* The ``File'' menu *}
-
-text {*
- Due to Java Applet security restrictions this menu is only available
- in the full application version. The meaning of the menu items is as
- follows:
-
- \begin{description}
-
- \item[Open \dots] Open a new graph file.
-
- \item[Export to PostScript] Outputs the current graph in Postscript
- format, appropriately scaled to fit on one single sheet of A4 paper.
- The resulting file can be printed directly.
-
- \item[Export to EPS] Outputs the current graph in Encapsulated
- Postscript format. The resulting file can be included in other
- documents.
-
- \item[Quit] Quit the graph browser.
-
- \end{description}
-*}
-
-
-subsection {* Syntax of graph definition files *}
-
-text {*
- A graph definition file has the following syntax:
-
- \begin{center}\small
- \begin{tabular}{rcl}
- @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\
- @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}
- \end{tabular}
- \end{center}
-
- The meaning of the items in a vertex description is as follows:
-
- \begin{description}
-
- \item[@{text vertex_name}] The name of the vertex.
-
- \item[@{text vertex_ID}] The vertex identifier. Note that there may
- be several vertices with equal names, whereas identifiers must be
- unique.
-
- \item[@{text dir_name}] The name of the ``directory'' the vertex
- should be placed in. A ``@{verbatim "+"}'' sign after @{text
- dir_name} indicates that the nodes in the directory are initially
- visible. Directories are initially invisible by default.
-
- \item[@{text 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 ``@{verbatim "<"}''
- sign before the list means that successor nodes are listed, a
- ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If
- neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the
- browser assumes that successor nodes are listed.
-
- \end{description}
-*}
-
-
section {* Creating Isabelle session directories
\label{sec:tool-mkdir} *}
--- a/doc-src/System/Thy/document/Interfaces.tex Sat Jul 28 13:18:34 2012 +0200
+++ b/doc-src/System/Thy/document/Interfaces.tex Sat Jul 28 13:29:56 2012 +0200
@@ -131,6 +131,195 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{Theory graph browser \label{sec:browse}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The Isabelle graph browser is a general tool for visualizing
+ dependency graphs. Certain nodes of the graph (i.e.\ theories) can
+ be grouped together in ``directories'', whose contents may be
+ hidden, thus enabling the user to collapse irrelevant portions of
+ information. The browser is written in Java, it can be used both as
+ a stand-alone application and as an applet. Note that the option
+ \verb|-g| of \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} creates
+ graph presentations in batch mode for inclusion in session
+ documents.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Invoking the graph browser%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The stand-alone version of the graph browser is wrapped up as an
+ Isabelle tool called \indexdef{}{tool}{browser}\hypertarget{tool.browser}{\hyperlink{tool.browser}{\mbox{\isa{\isatt{browser}}}}}:
+
+\begin{ttbox}
+Usage: browser [OPTIONS] [GRAPHFILE]
+
+ Options are:
+ -b Admin/build only
+ -c cleanup -- remove GRAPHFILE after use
+ -o FILE output to FILE (ps, eps, pdf)
+\end{ttbox}
+ When no filename is specified, the browser automatically changes to
+ the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}.
+
+ \medskip The \verb|-b| option indicates that this is for
+ administrative build only, i.e.\ no browser popup if no files are
+ given.
+
+ The \verb|-c| option causes the input file to be removed
+ after use.
+
+ The \verb|-o| option indicates batch-mode operation, with the
+ output written to the indicated file; note that \verb|pdf|
+ produces an \verb|eps| copy as well.
+
+ \medskip The applet version of the browser is part of the standard
+ WWW theory presentation, see the link ``theory dependencies'' within
+ each session index.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Using the graph browser%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The browser's main window, which is shown in
+ \figref{fig:browserwindow}, consists of two sub-windows. In the
+ left sub-window, the directory tree is displayed. The graph itself
+ is displayed in the right sub-window.
+
+ \begin{figure}[ht]
+ \includegraphics[width=\textwidth]{browser_screenshot}
+ \caption{\label{fig:browserwindow} Browser main window}
+ \end{figure}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{The directory tree window%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+We describe 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 sub-window, the names
+ of nodes corresponding to folded directories are enclosed in square
+ brackets and displayed in red color.
+
+ \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
+ sub-window.
+
+ \item Blue arrows stand before ordinary node names. When clicking on
+ such a name (i.e.\ that of a theory), 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}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{The graph display window%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+When pointing on an ordinary node, an upward and a downward arrow is
+ shown. Initially, both of these arrows are green. Clicking on the
+ upward or downward arrow collapses all predecessor or successor
+ nodes, respectively. The arrow's color then changes to red,
+ indicating that the predecessor or successor nodes are currently
+ collapsed. The node corresponding to the collapsed nodes has the
+ name ``\verb|[....]|''. To uncollapse the nodes again, simply
+ click on the red arrow or on the node with the name ``\verb|[....]|''. Similar to the directory browser, the contents of
+ theory files can be displayed by double clicking on the
+ corresponding node.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{The ``File'' menu%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Due to Java Applet security restrictions this menu is only available
+ in the full application version. The meaning of the menu items is as
+ follows:
+
+ \begin{description}
+
+ \item[Open \dots] Open a new graph file.
+
+ \item[Export to PostScript] Outputs the current graph in Postscript
+ format, appropriately scaled to fit on one single sheet of A4 paper.
+ The resulting file can be printed directly.
+
+ \item[Export to EPS] Outputs the current graph in Encapsulated
+ Postscript format. The resulting file can be included in other
+ documents.
+
+ \item[Quit] Quit the graph browser.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Syntax of graph definition files%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A graph definition file has the following syntax:
+
+ \begin{center}\small
+ \begin{tabular}{rcl}
+ \isa{graph} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7B}{\isacharbraceleft}}\ vertex{\isaliteral{22}{\isachardoublequote}}}~\verb|;|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequote}}} \\
+ \isa{vertex} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}vertex{\isaliteral{5F}{\isacharunderscore}}name\ vertex{\isaliteral{5F}{\isacharunderscore}}ID\ dir{\isaliteral{5F}{\isacharunderscore}}name\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}}~\verb|+|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ path\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}}~\verb|<|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}~\verb|>|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\ vertex{\isaliteral{5F}{\isacharunderscore}}ID\ {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}
+ \end{tabular}
+ \end{center}
+
+ The meaning of the items in a vertex description is as follows:
+
+ \begin{description}
+
+ \item[\isa{vertex{\isaliteral{5F}{\isacharunderscore}}name}] The name of the vertex.
+
+ \item[\isa{vertex{\isaliteral{5F}{\isacharunderscore}}ID}] The vertex identifier. Note that there may
+ be several vertices with equal names, whereas identifiers must be
+ unique.
+
+ \item[\isa{dir{\isaliteral{5F}{\isacharunderscore}}name}] The name of the ``directory'' the vertex
+ should be placed in. A ``\verb|+|'' sign after \isa{dir{\isaliteral{5F}{\isacharunderscore}}name} indicates that the nodes in the directory are initially
+ visible. Directories are initially invisible by default.
+
+ \item[\isa{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 ``\verb|<|''
+ sign before the list means that successor nodes are listed, a
+ ``\verb|>|'' sign means that predecessor nodes are listed. If
+ neither ``\verb|<|'' nor ``\verb|>|'' is found, the
+ browser assumes that successor nodes are listed.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/System/Thy/document/Presentation.tex Sat Jul 28 13:18:34 2012 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex Sat Jul 28 13:29:56 2012 +0200
@@ -168,197 +168,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Browsing theory graphs \label{sec:browse}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\index{theory graph browser|bold}
-
- The Isabelle graph browser is a general tool for visualizing
- dependency graphs. Certain nodes of the graph (i.e.~theories) can
- be grouped together in ``directories'', whose contents may be
- hidden, thus enabling the user to collapse irrelevant portions of
- information. The browser is written in Java, it can be used both as
- a stand-alone application and as an applet. Note that the option
- \verb|-g| of \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} creates
- graph presentations in batch mode for inclusion in session
- documents.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Invoking the graph browser%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The stand-alone version of the graph browser is wrapped up as an
- Isabelle tool called \indexdef{}{tool}{browser}\hypertarget{tool.browser}{\hyperlink{tool.browser}{\mbox{\isa{\isatt{browser}}}}}:
-
-\begin{ttbox}
-Usage: browser [OPTIONS] [GRAPHFILE]
-
- Options are:
- -b Admin/build only
- -c cleanup -- remove GRAPHFILE after use
- -o FILE output to FILE (ps, eps, pdf)
-\end{ttbox}
- When no filename is specified, the browser automatically changes to
- the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}.
-
- \medskip The \verb|-b| option indicates that this is for
- administrative build only, i.e.\ no browser popup if no files are
- given.
-
- The \verb|-c| option causes the input file to be removed
- after use.
-
- The \verb|-o| option indicates batch-mode operation, with the
- output written to the indicated file; note that \verb|pdf|
- produces an \verb|eps| copy as well.
-
- \medskip The applet version of the browser is part of the standard
- WWW theory presentation, see the link ``theory dependencies'' within
- each session index.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Using the graph browser%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The browser's main window, which is shown in
- \figref{fig:browserwindow}, consists of two sub-windows. In the
- left sub-window, the directory tree is displayed. The graph itself
- is displayed in the right sub-window.
-
- \begin{figure}[ht]
- \includegraphics[width=\textwidth]{browser_screenshot}
- \caption{\label{fig:browserwindow} Browser main window}
- \end{figure}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{The directory tree window%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-We describe 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 sub-window, the names
- of nodes corresponding to folded directories are enclosed in square
- brackets and displayed in red color.
-
- \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
- sub-window.
-
- \item Blue arrows stand before ordinary node names. When clicking on
- such a name (i.e.\ that of a theory), 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}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{The graph display window%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-When pointing on an ordinary node, an upward and a downward arrow is
- shown. Initially, both of these arrows are green. Clicking on the
- upward or downward arrow collapses all predecessor or successor
- nodes, respectively. The arrow's color then changes to red,
- indicating that the predecessor or successor nodes are currently
- collapsed. The node corresponding to the collapsed nodes has the
- name ``\verb|[....]|''. To uncollapse the nodes again, simply
- click on the red arrow or on the node with the name ``\verb|[....]|''. Similar to the directory browser, the contents of
- theory files can be displayed by double clicking on the
- corresponding node.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{The ``File'' menu%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Due to Java Applet security restrictions this menu is only available
- in the full application version. The meaning of the menu items is as
- follows:
-
- \begin{description}
-
- \item[Open \dots] Open a new graph file.
-
- \item[Export to PostScript] Outputs the current graph in Postscript
- format, appropriately scaled to fit on one single sheet of A4 paper.
- The resulting file can be printed directly.
-
- \item[Export to EPS] Outputs the current graph in Encapsulated
- Postscript format. The resulting file can be included in other
- documents.
-
- \item[Quit] Quit the graph browser.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Syntax of graph definition files%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-A graph definition file has the following syntax:
-
- \begin{center}\small
- \begin{tabular}{rcl}
- \isa{graph} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7B}{\isacharbraceleft}}\ vertex{\isaliteral{22}{\isachardoublequote}}}~\verb|;|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequote}}} \\
- \isa{vertex} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}vertex{\isaliteral{5F}{\isacharunderscore}}name\ vertex{\isaliteral{5F}{\isacharunderscore}}ID\ dir{\isaliteral{5F}{\isacharunderscore}}name\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}}~\verb|+|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ path\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}}~\verb|<|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}~\verb|>|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\ vertex{\isaliteral{5F}{\isacharunderscore}}ID\ {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}
- \end{tabular}
- \end{center}
-
- The meaning of the items in a vertex description is as follows:
-
- \begin{description}
-
- \item[\isa{vertex{\isaliteral{5F}{\isacharunderscore}}name}] The name of the vertex.
-
- \item[\isa{vertex{\isaliteral{5F}{\isacharunderscore}}ID}] The vertex identifier. Note that there may
- be several vertices with equal names, whereas identifiers must be
- unique.
-
- \item[\isa{dir{\isaliteral{5F}{\isacharunderscore}}name}] The name of the ``directory'' the vertex
- should be placed in. A ``\verb|+|'' sign after \isa{dir{\isaliteral{5F}{\isacharunderscore}}name} indicates that the nodes in the directory are initially
- visible. Directories are initially invisible by default.
-
- \item[\isa{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 ``\verb|<|''
- sign before the list means that successor nodes are listed, a
- ``\verb|>|'' sign means that predecessor nodes are listed. If
- neither ``\verb|<|'' nor ``\verb|>|'' is found, the
- browser assumes that successor nodes are listed.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{Creating Isabelle session directories
\label{sec:tool-mkdir}%
}