1.1 --- a/doc-src/System/Thy/Interfaces.thy Sat Jul 28 13:18:34 2012 +0200
1.2 +++ b/doc-src/System/Thy/Interfaces.thy Sat Jul 28 13:29:56 2012 +0200
1.3 @@ -105,4 +105,180 @@
1.4 infrastructure itself. Invoking @{ML Isar.loop}~@{verbatim "();"}
1.5 in ML will return to the Isar toplevel. *}
1.6
1.7 +
1.8 +
1.9 +section {* Theory graph browser \label{sec:browse} *}
1.10 +
1.11 +text {* The Isabelle graph browser is a general tool for visualizing
1.12 + dependency graphs. Certain nodes of the graph (i.e.\ theories) can
1.13 + be grouped together in ``directories'', whose contents may be
1.14 + hidden, thus enabling the user to collapse irrelevant portions of
1.15 + information. The browser is written in Java, it can be used both as
1.16 + a stand-alone application and as an applet. Note that the option
1.17 + @{verbatim "-g"} of @{verbatim isabelle} @{tool_ref usedir} creates
1.18 + graph presentations in batch mode for inclusion in session
1.19 + documents. *}
1.20 +
1.21 +
1.22 +subsection {* Invoking the graph browser *}
1.23 +
1.24 +text {*
1.25 + The stand-alone version of the graph browser is wrapped up as an
1.26 + Isabelle tool called @{tool_def browser}:
1.27 +
1.28 +\begin{ttbox}
1.29 +Usage: browser [OPTIONS] [GRAPHFILE]
1.30 +
1.31 + Options are:
1.32 + -b Admin/build only
1.33 + -c cleanup -- remove GRAPHFILE after use
1.34 + -o FILE output to FILE (ps, eps, pdf)
1.35 +\end{ttbox}
1.36 + When no filename is specified, the browser automatically changes to
1.37 + the directory @{setting ISABELLE_BROWSER_INFO}.
1.38 +
1.39 + \medskip The @{verbatim "-b"} option indicates that this is for
1.40 + administrative build only, i.e.\ no browser popup if no files are
1.41 + given.
1.42 +
1.43 + The @{verbatim "-c"} option causes the input file to be removed
1.44 + after use.
1.45 +
1.46 + The @{verbatim "-o"} option indicates batch-mode operation, with the
1.47 + output written to the indicated file; note that @{verbatim pdf}
1.48 + produces an @{verbatim eps} copy as well.
1.49 +
1.50 + \medskip The applet version of the browser is part of the standard
1.51 + WWW theory presentation, see the link ``theory dependencies'' within
1.52 + each session index.
1.53 +*}
1.54 +
1.55 +
1.56 +subsection {* Using the graph browser *}
1.57 +
1.58 +text {*
1.59 + The browser's main window, which is shown in
1.60 + \figref{fig:browserwindow}, consists of two sub-windows. In the
1.61 + left sub-window, the directory tree is displayed. The graph itself
1.62 + is displayed in the right sub-window.
1.63 +
1.64 + \begin{figure}[ht]
1.65 + \includegraphics[width=\textwidth]{browser_screenshot}
1.66 + \caption{\label{fig:browserwindow} Browser main window}
1.67 + \end{figure}
1.68 +*}
1.69 +
1.70 +
1.71 +subsubsection {* The directory tree window *}
1.72 +
1.73 +text {*
1.74 + We describe the usage of the directory browser and the meaning of
1.75 + the different items in the browser window.
1.76 +
1.77 + \begin{itemize}
1.78 +
1.79 + \item A red arrow before a directory name indicates that the
1.80 + directory is currently ``folded'', i.e.~the nodes in this directory
1.81 + are collapsed to one single node. In the right sub-window, the names
1.82 + of nodes corresponding to folded directories are enclosed in square
1.83 + brackets and displayed in red color.
1.84 +
1.85 + \item A green downward arrow before a directory name indicates that
1.86 + the directory is currently ``unfolded''. It can be folded by
1.87 + clicking on the directory name. Clicking on the name for a second
1.88 + time unfolds the directory again. Alternatively, a directory can
1.89 + also be unfolded by clicking on the corresponding node in the right
1.90 + sub-window.
1.91 +
1.92 + \item Blue arrows stand before ordinary node names. When clicking on
1.93 + such a name (i.e.\ that of a theory), the graph display window
1.94 + focuses to the corresponding node. Double clicking invokes a text
1.95 + viewer window in which the contents of the theory file are
1.96 + displayed.
1.97 +
1.98 + \end{itemize}
1.99 +*}
1.100 +
1.101 +
1.102 +subsubsection {* The graph display window *}
1.103 +
1.104 +text {*
1.105 + When pointing on an ordinary node, an upward and a downward arrow is
1.106 + shown. Initially, both of these arrows are green. Clicking on the
1.107 + upward or downward arrow collapses all predecessor or successor
1.108 + nodes, respectively. The arrow's color then changes to red,
1.109 + indicating that the predecessor or successor nodes are currently
1.110 + collapsed. The node corresponding to the collapsed nodes has the
1.111 + name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply
1.112 + click on the red arrow or on the node with the name ``@{verbatim
1.113 + "[....]"}''. Similar to the directory browser, the contents of
1.114 + theory files can be displayed by double clicking on the
1.115 + corresponding node.
1.116 +*}
1.117 +
1.118 +
1.119 +subsubsection {* The ``File'' menu *}
1.120 +
1.121 +text {*
1.122 + Due to Java Applet security restrictions this menu is only available
1.123 + in the full application version. The meaning of the menu items is as
1.124 + follows:
1.125 +
1.126 + \begin{description}
1.127 +
1.128 + \item[Open \dots] Open a new graph file.
1.129 +
1.130 + \item[Export to PostScript] Outputs the current graph in Postscript
1.131 + format, appropriately scaled to fit on one single sheet of A4 paper.
1.132 + The resulting file can be printed directly.
1.133 +
1.134 + \item[Export to EPS] Outputs the current graph in Encapsulated
1.135 + Postscript format. The resulting file can be included in other
1.136 + documents.
1.137 +
1.138 + \item[Quit] Quit the graph browser.
1.139 +
1.140 + \end{description}
1.141 +*}
1.142 +
1.143 +
1.144 +subsection {* Syntax of graph definition files *}
1.145 +
1.146 +text {*
1.147 + A graph definition file has the following syntax:
1.148 +
1.149 + \begin{center}\small
1.150 + \begin{tabular}{rcl}
1.151 + @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\
1.152 + @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}
1.153 + \end{tabular}
1.154 + \end{center}
1.155 +
1.156 + The meaning of the items in a vertex description is as follows:
1.157 +
1.158 + \begin{description}
1.159 +
1.160 + \item[@{text vertex_name}] The name of the vertex.
1.161 +
1.162 + \item[@{text vertex_ID}] The vertex identifier. Note that there may
1.163 + be several vertices with equal names, whereas identifiers must be
1.164 + unique.
1.165 +
1.166 + \item[@{text dir_name}] The name of the ``directory'' the vertex
1.167 + should be placed in. A ``@{verbatim "+"}'' sign after @{text
1.168 + dir_name} indicates that the nodes in the directory are initially
1.169 + visible. Directories are initially invisible by default.
1.170 +
1.171 + \item[@{text path}] The path of the corresponding theory file. This
1.172 + is specified relatively to the path of the graph definition file.
1.173 +
1.174 + \item[List of successor/predecessor nodes] A ``@{verbatim "<"}''
1.175 + sign before the list means that successor nodes are listed, a
1.176 + ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If
1.177 + neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the
1.178 + browser assumes that successor nodes are listed.
1.179 +
1.180 + \end{description}
1.181 +*}
1.182 +
1.183 end
1.184 \ No newline at end of file
2.1 --- a/doc-src/System/Thy/Presentation.thy Sat Jul 28 13:18:34 2012 +0200
2.2 +++ b/doc-src/System/Thy/Presentation.thy Sat Jul 28 13:29:56 2012 +0200
2.3 @@ -157,185 +157,6 @@
2.4 *}
2.5
2.6
2.7 -section {* Browsing theory graphs \label{sec:browse} *}
2.8 -
2.9 -text {*
2.10 - \index{theory graph browser|bold}
2.11 -
2.12 - The Isabelle graph browser is a general tool for visualizing
2.13 - dependency graphs. Certain nodes of the graph (i.e.~theories) can
2.14 - be grouped together in ``directories'', whose contents may be
2.15 - hidden, thus enabling the user to collapse irrelevant portions of
2.16 - information. The browser is written in Java, it can be used both as
2.17 - a stand-alone application and as an applet. Note that the option
2.18 - @{verbatim "-g"} of @{verbatim isabelle} @{tool_ref usedir} creates
2.19 - graph presentations in batch mode for inclusion in session
2.20 - documents.
2.21 -*}
2.22 -
2.23 -
2.24 -subsection {* Invoking the graph browser *}
2.25 -
2.26 -text {*
2.27 - The stand-alone version of the graph browser is wrapped up as an
2.28 - Isabelle tool called @{tool_def browser}:
2.29 -
2.30 -\begin{ttbox}
2.31 -Usage: browser [OPTIONS] [GRAPHFILE]
2.32 -
2.33 - Options are:
2.34 - -b Admin/build only
2.35 - -c cleanup -- remove GRAPHFILE after use
2.36 - -o FILE output to FILE (ps, eps, pdf)
2.37 -\end{ttbox}
2.38 - When no filename is specified, the browser automatically changes to
2.39 - the directory @{setting ISABELLE_BROWSER_INFO}.
2.40 -
2.41 - \medskip The @{verbatim "-b"} option indicates that this is for
2.42 - administrative build only, i.e.\ no browser popup if no files are
2.43 - given.
2.44 -
2.45 - The @{verbatim "-c"} option causes the input file to be removed
2.46 - after use.
2.47 -
2.48 - The @{verbatim "-o"} option indicates batch-mode operation, with the
2.49 - output written to the indicated file; note that @{verbatim pdf}
2.50 - produces an @{verbatim eps} copy as well.
2.51 -
2.52 - \medskip The applet version of the browser is part of the standard
2.53 - WWW theory presentation, see the link ``theory dependencies'' within
2.54 - each session index.
2.55 -*}
2.56 -
2.57 -
2.58 -subsection {* Using the graph browser *}
2.59 -
2.60 -text {*
2.61 - The browser's main window, which is shown in
2.62 - \figref{fig:browserwindow}, consists of two sub-windows. In the
2.63 - left sub-window, the directory tree is displayed. The graph itself
2.64 - is displayed in the right sub-window.
2.65 -
2.66 - \begin{figure}[ht]
2.67 - \includegraphics[width=\textwidth]{browser_screenshot}
2.68 - \caption{\label{fig:browserwindow} Browser main window}
2.69 - \end{figure}
2.70 -*}
2.71 -
2.72 -
2.73 -subsubsection {* The directory tree window *}
2.74 -
2.75 -text {*
2.76 - We describe the usage of the directory browser and the meaning of
2.77 - the different items in the browser window.
2.78 -
2.79 - \begin{itemize}
2.80 -
2.81 - \item A red arrow before a directory name indicates that the
2.82 - directory is currently ``folded'', i.e.~the nodes in this directory
2.83 - are collapsed to one single node. In the right sub-window, the names
2.84 - of nodes corresponding to folded directories are enclosed in square
2.85 - brackets and displayed in red color.
2.86 -
2.87 - \item A green downward arrow before a directory name indicates that
2.88 - the directory is currently ``unfolded''. It can be folded by
2.89 - clicking on the directory name. Clicking on the name for a second
2.90 - time unfolds the directory again. Alternatively, a directory can
2.91 - also be unfolded by clicking on the corresponding node in the right
2.92 - sub-window.
2.93 -
2.94 - \item Blue arrows stand before ordinary node names. When clicking on
2.95 - such a name (i.e.\ that of a theory), the graph display window
2.96 - focuses to the corresponding node. Double clicking invokes a text
2.97 - viewer window in which the contents of the theory file are
2.98 - displayed.
2.99 -
2.100 - \end{itemize}
2.101 -*}
2.102 -
2.103 -
2.104 -subsubsection {* The graph display window *}
2.105 -
2.106 -text {*
2.107 - When pointing on an ordinary node, an upward and a downward arrow is
2.108 - shown. Initially, both of these arrows are green. Clicking on the
2.109 - upward or downward arrow collapses all predecessor or successor
2.110 - nodes, respectively. The arrow's color then changes to red,
2.111 - indicating that the predecessor or successor nodes are currently
2.112 - collapsed. The node corresponding to the collapsed nodes has the
2.113 - name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply
2.114 - click on the red arrow or on the node with the name ``@{verbatim
2.115 - "[....]"}''. Similar to the directory browser, the contents of
2.116 - theory files can be displayed by double clicking on the
2.117 - corresponding node.
2.118 -*}
2.119 -
2.120 -
2.121 -subsubsection {* The ``File'' menu *}
2.122 -
2.123 -text {*
2.124 - Due to Java Applet security restrictions this menu is only available
2.125 - in the full application version. The meaning of the menu items is as
2.126 - follows:
2.127 -
2.128 - \begin{description}
2.129 -
2.130 - \item[Open \dots] Open a new graph file.
2.131 -
2.132 - \item[Export to PostScript] Outputs the current graph in Postscript
2.133 - format, appropriately scaled to fit on one single sheet of A4 paper.
2.134 - The resulting file can be printed directly.
2.135 -
2.136 - \item[Export to EPS] Outputs the current graph in Encapsulated
2.137 - Postscript format. The resulting file can be included in other
2.138 - documents.
2.139 -
2.140 - \item[Quit] Quit the graph browser.
2.141 -
2.142 - \end{description}
2.143 -*}
2.144 -
2.145 -
2.146 -subsection {* Syntax of graph definition files *}
2.147 -
2.148 -text {*
2.149 - A graph definition file has the following syntax:
2.150 -
2.151 - \begin{center}\small
2.152 - \begin{tabular}{rcl}
2.153 - @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\
2.154 - @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}
2.155 - \end{tabular}
2.156 - \end{center}
2.157 -
2.158 - The meaning of the items in a vertex description is as follows:
2.159 -
2.160 - \begin{description}
2.161 -
2.162 - \item[@{text vertex_name}] The name of the vertex.
2.163 -
2.164 - \item[@{text vertex_ID}] The vertex identifier. Note that there may
2.165 - be several vertices with equal names, whereas identifiers must be
2.166 - unique.
2.167 -
2.168 - \item[@{text dir_name}] The name of the ``directory'' the vertex
2.169 - should be placed in. A ``@{verbatim "+"}'' sign after @{text
2.170 - dir_name} indicates that the nodes in the directory are initially
2.171 - visible. Directories are initially invisible by default.
2.172 -
2.173 - \item[@{text path}] The path of the corresponding theory file. This
2.174 - is specified relatively to the path of the graph definition file.
2.175 -
2.176 - \item[List of successor/predecessor nodes] A ``@{verbatim "<"}''
2.177 - sign before the list means that successor nodes are listed, a
2.178 - ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If
2.179 - neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the
2.180 - browser assumes that successor nodes are listed.
2.181 -
2.182 - \end{description}
2.183 -*}
2.184 -
2.185 -
2.186 section {* Creating Isabelle session directories
2.187 \label{sec:tool-mkdir} *}
2.188
3.1 --- a/doc-src/System/Thy/document/Interfaces.tex Sat Jul 28 13:18:34 2012 +0200
3.2 +++ b/doc-src/System/Thy/document/Interfaces.tex Sat Jul 28 13:29:56 2012 +0200
3.3 @@ -131,6 +131,195 @@
3.4 \end{isamarkuptext}%
3.5 \isamarkuptrue%
3.6 %
3.7 +\isamarkupsection{Theory graph browser \label{sec:browse}%
3.8 +}
3.9 +\isamarkuptrue%
3.10 +%
3.11 +\begin{isamarkuptext}%
3.12 +The Isabelle graph browser is a general tool for visualizing
3.13 + dependency graphs. Certain nodes of the graph (i.e.\ theories) can
3.14 + be grouped together in ``directories'', whose contents may be
3.15 + hidden, thus enabling the user to collapse irrelevant portions of
3.16 + information. The browser is written in Java, it can be used both as
3.17 + a stand-alone application and as an applet. Note that the option
3.18 + \verb|-g| of \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} creates
3.19 + graph presentations in batch mode for inclusion in session
3.20 + documents.%
3.21 +\end{isamarkuptext}%
3.22 +\isamarkuptrue%
3.23 +%
3.24 +\isamarkupsubsection{Invoking the graph browser%
3.25 +}
3.26 +\isamarkuptrue%
3.27 +%
3.28 +\begin{isamarkuptext}%
3.29 +The stand-alone version of the graph browser is wrapped up as an
3.30 + Isabelle tool called \indexdef{}{tool}{browser}\hypertarget{tool.browser}{\hyperlink{tool.browser}{\mbox{\isa{\isatt{browser}}}}}:
3.31 +
3.32 +\begin{ttbox}
3.33 +Usage: browser [OPTIONS] [GRAPHFILE]
3.34 +
3.35 + Options are:
3.36 + -b Admin/build only
3.37 + -c cleanup -- remove GRAPHFILE after use
3.38 + -o FILE output to FILE (ps, eps, pdf)
3.39 +\end{ttbox}
3.40 + When no filename is specified, the browser automatically changes to
3.41 + the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}.
3.42 +
3.43 + \medskip The \verb|-b| option indicates that this is for
3.44 + administrative build only, i.e.\ no browser popup if no files are
3.45 + given.
3.46 +
3.47 + The \verb|-c| option causes the input file to be removed
3.48 + after use.
3.49 +
3.50 + The \verb|-o| option indicates batch-mode operation, with the
3.51 + output written to the indicated file; note that \verb|pdf|
3.52 + produces an \verb|eps| copy as well.
3.53 +
3.54 + \medskip The applet version of the browser is part of the standard
3.55 + WWW theory presentation, see the link ``theory dependencies'' within
3.56 + each session index.%
3.57 +\end{isamarkuptext}%
3.58 +\isamarkuptrue%
3.59 +%
3.60 +\isamarkupsubsection{Using the graph browser%
3.61 +}
3.62 +\isamarkuptrue%
3.63 +%
3.64 +\begin{isamarkuptext}%
3.65 +The browser's main window, which is shown in
3.66 + \figref{fig:browserwindow}, consists of two sub-windows. In the
3.67 + left sub-window, the directory tree is displayed. The graph itself
3.68 + is displayed in the right sub-window.
3.69 +
3.70 + \begin{figure}[ht]
3.71 + \includegraphics[width=\textwidth]{browser_screenshot}
3.72 + \caption{\label{fig:browserwindow} Browser main window}
3.73 + \end{figure}%
3.74 +\end{isamarkuptext}%
3.75 +\isamarkuptrue%
3.76 +%
3.77 +\isamarkupsubsubsection{The directory tree window%
3.78 +}
3.79 +\isamarkuptrue%
3.80 +%
3.81 +\begin{isamarkuptext}%
3.82 +We describe the usage of the directory browser and the meaning of
3.83 + the different items in the browser window.
3.84 +
3.85 + \begin{itemize}
3.86 +
3.87 + \item A red arrow before a directory name indicates that the
3.88 + directory is currently ``folded'', i.e.~the nodes in this directory
3.89 + are collapsed to one single node. In the right sub-window, the names
3.90 + of nodes corresponding to folded directories are enclosed in square
3.91 + brackets and displayed in red color.
3.92 +
3.93 + \item A green downward arrow before a directory name indicates that
3.94 + the directory is currently ``unfolded''. It can be folded by
3.95 + clicking on the directory name. Clicking on the name for a second
3.96 + time unfolds the directory again. Alternatively, a directory can
3.97 + also be unfolded by clicking on the corresponding node in the right
3.98 + sub-window.
3.99 +
3.100 + \item Blue arrows stand before ordinary node names. When clicking on
3.101 + such a name (i.e.\ that of a theory), the graph display window
3.102 + focuses to the corresponding node. Double clicking invokes a text
3.103 + viewer window in which the contents of the theory file are
3.104 + displayed.
3.105 +
3.106 + \end{itemize}%
3.107 +\end{isamarkuptext}%
3.108 +\isamarkuptrue%
3.109 +%
3.110 +\isamarkupsubsubsection{The graph display window%
3.111 +}
3.112 +\isamarkuptrue%
3.113 +%
3.114 +\begin{isamarkuptext}%
3.115 +When pointing on an ordinary node, an upward and a downward arrow is
3.116 + shown. Initially, both of these arrows are green. Clicking on the
3.117 + upward or downward arrow collapses all predecessor or successor
3.118 + nodes, respectively. The arrow's color then changes to red,
3.119 + indicating that the predecessor or successor nodes are currently
3.120 + collapsed. The node corresponding to the collapsed nodes has the
3.121 + name ``\verb|[....]|''. To uncollapse the nodes again, simply
3.122 + click on the red arrow or on the node with the name ``\verb|[....]|''. Similar to the directory browser, the contents of
3.123 + theory files can be displayed by double clicking on the
3.124 + corresponding node.%
3.125 +\end{isamarkuptext}%
3.126 +\isamarkuptrue%
3.127 +%
3.128 +\isamarkupsubsubsection{The ``File'' menu%
3.129 +}
3.130 +\isamarkuptrue%
3.131 +%
3.132 +\begin{isamarkuptext}%
3.133 +Due to Java Applet security restrictions this menu is only available
3.134 + in the full application version. The meaning of the menu items is as
3.135 + follows:
3.136 +
3.137 + \begin{description}
3.138 +
3.139 + \item[Open \dots] Open a new graph file.
3.140 +
3.141 + \item[Export to PostScript] Outputs the current graph in Postscript
3.142 + format, appropriately scaled to fit on one single sheet of A4 paper.
3.143 + The resulting file can be printed directly.
3.144 +
3.145 + \item[Export to EPS] Outputs the current graph in Encapsulated
3.146 + Postscript format. The resulting file can be included in other
3.147 + documents.
3.148 +
3.149 + \item[Quit] Quit the graph browser.
3.150 +
3.151 + \end{description}%
3.152 +\end{isamarkuptext}%
3.153 +\isamarkuptrue%
3.154 +%
3.155 +\isamarkupsubsection{Syntax of graph definition files%
3.156 +}
3.157 +\isamarkuptrue%
3.158 +%
3.159 +\begin{isamarkuptext}%
3.160 +A graph definition file has the following syntax:
3.161 +
3.162 + \begin{center}\small
3.163 + \begin{tabular}{rcl}
3.164 + \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}}} \\
3.165 + \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}}}
3.166 + \end{tabular}
3.167 + \end{center}
3.168 +
3.169 + The meaning of the items in a vertex description is as follows:
3.170 +
3.171 + \begin{description}
3.172 +
3.173 + \item[\isa{vertex{\isaliteral{5F}{\isacharunderscore}}name}] The name of the vertex.
3.174 +
3.175 + \item[\isa{vertex{\isaliteral{5F}{\isacharunderscore}}ID}] The vertex identifier. Note that there may
3.176 + be several vertices with equal names, whereas identifiers must be
3.177 + unique.
3.178 +
3.179 + \item[\isa{dir{\isaliteral{5F}{\isacharunderscore}}name}] The name of the ``directory'' the vertex
3.180 + should be placed in. A ``\verb|+|'' sign after \isa{dir{\isaliteral{5F}{\isacharunderscore}}name} indicates that the nodes in the directory are initially
3.181 + visible. Directories are initially invisible by default.
3.182 +
3.183 + \item[\isa{path}] The path of the corresponding theory file. This
3.184 + is specified relatively to the path of the graph definition file.
3.185 +
3.186 + \item[List of successor/predecessor nodes] A ``\verb|<|''
3.187 + sign before the list means that successor nodes are listed, a
3.188 + ``\verb|>|'' sign means that predecessor nodes are listed. If
3.189 + neither ``\verb|<|'' nor ``\verb|>|'' is found, the
3.190 + browser assumes that successor nodes are listed.
3.191 +
3.192 + \end{description}%
3.193 +\end{isamarkuptext}%
3.194 +\isamarkuptrue%
3.195 +%
3.196 \isadelimtheory
3.197 %
3.198 \endisadelimtheory
4.1 --- a/doc-src/System/Thy/document/Presentation.tex Sat Jul 28 13:18:34 2012 +0200
4.2 +++ b/doc-src/System/Thy/document/Presentation.tex Sat Jul 28 13:29:56 2012 +0200
4.3 @@ -168,197 +168,6 @@
4.4 \end{isamarkuptext}%
4.5 \isamarkuptrue%
4.6 %
4.7 -\isamarkupsection{Browsing theory graphs \label{sec:browse}%
4.8 -}
4.9 -\isamarkuptrue%
4.10 -%
4.11 -\begin{isamarkuptext}%
4.12 -\index{theory graph browser|bold}
4.13 -
4.14 - The Isabelle graph browser is a general tool for visualizing
4.15 - dependency graphs. Certain nodes of the graph (i.e.~theories) can
4.16 - be grouped together in ``directories'', whose contents may be
4.17 - hidden, thus enabling the user to collapse irrelevant portions of
4.18 - information. The browser is written in Java, it can be used both as
4.19 - a stand-alone application and as an applet. Note that the option
4.20 - \verb|-g| of \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} creates
4.21 - graph presentations in batch mode for inclusion in session
4.22 - documents.%
4.23 -\end{isamarkuptext}%
4.24 -\isamarkuptrue%
4.25 -%
4.26 -\isamarkupsubsection{Invoking the graph browser%
4.27 -}
4.28 -\isamarkuptrue%
4.29 -%
4.30 -\begin{isamarkuptext}%
4.31 -The stand-alone version of the graph browser is wrapped up as an
4.32 - Isabelle tool called \indexdef{}{tool}{browser}\hypertarget{tool.browser}{\hyperlink{tool.browser}{\mbox{\isa{\isatt{browser}}}}}:
4.33 -
4.34 -\begin{ttbox}
4.35 -Usage: browser [OPTIONS] [GRAPHFILE]
4.36 -
4.37 - Options are:
4.38 - -b Admin/build only
4.39 - -c cleanup -- remove GRAPHFILE after use
4.40 - -o FILE output to FILE (ps, eps, pdf)
4.41 -\end{ttbox}
4.42 - When no filename is specified, the browser automatically changes to
4.43 - the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}.
4.44 -
4.45 - \medskip The \verb|-b| option indicates that this is for
4.46 - administrative build only, i.e.\ no browser popup if no files are
4.47 - given.
4.48 -
4.49 - The \verb|-c| option causes the input file to be removed
4.50 - after use.
4.51 -
4.52 - The \verb|-o| option indicates batch-mode operation, with the
4.53 - output written to the indicated file; note that \verb|pdf|
4.54 - produces an \verb|eps| copy as well.
4.55 -
4.56 - \medskip The applet version of the browser is part of the standard
4.57 - WWW theory presentation, see the link ``theory dependencies'' within
4.58 - each session index.%
4.59 -\end{isamarkuptext}%
4.60 -\isamarkuptrue%
4.61 -%
4.62 -\isamarkupsubsection{Using the graph browser%
4.63 -}
4.64 -\isamarkuptrue%
4.65 -%
4.66 -\begin{isamarkuptext}%
4.67 -The browser's main window, which is shown in
4.68 - \figref{fig:browserwindow}, consists of two sub-windows. In the
4.69 - left sub-window, the directory tree is displayed. The graph itself
4.70 - is displayed in the right sub-window.
4.71 -
4.72 - \begin{figure}[ht]
4.73 - \includegraphics[width=\textwidth]{browser_screenshot}
4.74 - \caption{\label{fig:browserwindow} Browser main window}
4.75 - \end{figure}%
4.76 -\end{isamarkuptext}%
4.77 -\isamarkuptrue%
4.78 -%
4.79 -\isamarkupsubsubsection{The directory tree window%
4.80 -}
4.81 -\isamarkuptrue%
4.82 -%
4.83 -\begin{isamarkuptext}%
4.84 -We describe the usage of the directory browser and the meaning of
4.85 - the different items in the browser window.
4.86 -
4.87 - \begin{itemize}
4.88 -
4.89 - \item A red arrow before a directory name indicates that the
4.90 - directory is currently ``folded'', i.e.~the nodes in this directory
4.91 - are collapsed to one single node. In the right sub-window, the names
4.92 - of nodes corresponding to folded directories are enclosed in square
4.93 - brackets and displayed in red color.
4.94 -
4.95 - \item A green downward arrow before a directory name indicates that
4.96 - the directory is currently ``unfolded''. It can be folded by
4.97 - clicking on the directory name. Clicking on the name for a second
4.98 - time unfolds the directory again. Alternatively, a directory can
4.99 - also be unfolded by clicking on the corresponding node in the right
4.100 - sub-window.
4.101 -
4.102 - \item Blue arrows stand before ordinary node names. When clicking on
4.103 - such a name (i.e.\ that of a theory), the graph display window
4.104 - focuses to the corresponding node. Double clicking invokes a text
4.105 - viewer window in which the contents of the theory file are
4.106 - displayed.
4.107 -
4.108 - \end{itemize}%
4.109 -\end{isamarkuptext}%
4.110 -\isamarkuptrue%
4.111 -%
4.112 -\isamarkupsubsubsection{The graph display window%
4.113 -}
4.114 -\isamarkuptrue%
4.115 -%
4.116 -\begin{isamarkuptext}%
4.117 -When pointing on an ordinary node, an upward and a downward arrow is
4.118 - shown. Initially, both of these arrows are green. Clicking on the
4.119 - upward or downward arrow collapses all predecessor or successor
4.120 - nodes, respectively. The arrow's color then changes to red,
4.121 - indicating that the predecessor or successor nodes are currently
4.122 - collapsed. The node corresponding to the collapsed nodes has the
4.123 - name ``\verb|[....]|''. To uncollapse the nodes again, simply
4.124 - click on the red arrow or on the node with the name ``\verb|[....]|''. Similar to the directory browser, the contents of
4.125 - theory files can be displayed by double clicking on the
4.126 - corresponding node.%
4.127 -\end{isamarkuptext}%
4.128 -\isamarkuptrue%
4.129 -%
4.130 -\isamarkupsubsubsection{The ``File'' menu%
4.131 -}
4.132 -\isamarkuptrue%
4.133 -%
4.134 -\begin{isamarkuptext}%
4.135 -Due to Java Applet security restrictions this menu is only available
4.136 - in the full application version. The meaning of the menu items is as
4.137 - follows:
4.138 -
4.139 - \begin{description}
4.140 -
4.141 - \item[Open \dots] Open a new graph file.
4.142 -
4.143 - \item[Export to PostScript] Outputs the current graph in Postscript
4.144 - format, appropriately scaled to fit on one single sheet of A4 paper.
4.145 - The resulting file can be printed directly.
4.146 -
4.147 - \item[Export to EPS] Outputs the current graph in Encapsulated
4.148 - Postscript format. The resulting file can be included in other
4.149 - documents.
4.150 -
4.151 - \item[Quit] Quit the graph browser.
4.152 -
4.153 - \end{description}%
4.154 -\end{isamarkuptext}%
4.155 -\isamarkuptrue%
4.156 -%
4.157 -\isamarkupsubsection{Syntax of graph definition files%
4.158 -}
4.159 -\isamarkuptrue%
4.160 -%
4.161 -\begin{isamarkuptext}%
4.162 -A graph definition file has the following syntax:
4.163 -
4.164 - \begin{center}\small
4.165 - \begin{tabular}{rcl}
4.166 - \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}}} \\
4.167 - \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}}}
4.168 - \end{tabular}
4.169 - \end{center}
4.170 -
4.171 - The meaning of the items in a vertex description is as follows:
4.172 -
4.173 - \begin{description}
4.174 -
4.175 - \item[\isa{vertex{\isaliteral{5F}{\isacharunderscore}}name}] The name of the vertex.
4.176 -
4.177 - \item[\isa{vertex{\isaliteral{5F}{\isacharunderscore}}ID}] The vertex identifier. Note that there may
4.178 - be several vertices with equal names, whereas identifiers must be
4.179 - unique.
4.180 -
4.181 - \item[\isa{dir{\isaliteral{5F}{\isacharunderscore}}name}] The name of the ``directory'' the vertex
4.182 - should be placed in. A ``\verb|+|'' sign after \isa{dir{\isaliteral{5F}{\isacharunderscore}}name} indicates that the nodes in the directory are initially
4.183 - visible. Directories are initially invisible by default.
4.184 -
4.185 - \item[\isa{path}] The path of the corresponding theory file. This
4.186 - is specified relatively to the path of the graph definition file.
4.187 -
4.188 - \item[List of successor/predecessor nodes] A ``\verb|<|''
4.189 - sign before the list means that successor nodes are listed, a
4.190 - ``\verb|>|'' sign means that predecessor nodes are listed. If
4.191 - neither ``\verb|<|'' nor ``\verb|>|'' is found, the
4.192 - browser assumes that successor nodes are listed.
4.193 -
4.194 - \end{description}%
4.195 -\end{isamarkuptext}%
4.196 -\isamarkuptrue%
4.197 -%
4.198 \isamarkupsection{Creating Isabelle session directories
4.199 \label{sec:tool-mkdir}%
4.200 }