--- a/src/Doc/ROOT Mon Jun 16 12:41:51 2014 +0200
+++ b/src/Doc/ROOT Mon Jun 16 12:52:20 2014 +0200
@@ -323,7 +323,6 @@
options [document_variants = "system", thy_output_source]
theories
Basics
- Interfaces
Sessions
Presentation
Scala
--- a/src/Doc/System/Interfaces.thy Mon Jun 16 12:41:51 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,250 +0,0 @@
-theory Interfaces
-imports Base
-begin
-
-chapter {* User interfaces *}
-
-text {*
- The default user-interface and Prover IDE is Isabelle/jEdit, which is
- described in a separate manual \cite{isabelle-jedit}.
-*}
-
-section {* Proof General / Emacs *}
-
-text {* The @{tool_def emacs} tool invokes a version of Emacs and
- Proof General\footnote{@{url "http://proofgeneral.inf.ed.ac.uk/"}} within the
- regular Isabelle settings environment (\secref{sec:settings}). This
- is more convenient than starting Emacs separately, loading the Proof
- General LISP files, and then attempting to start Isabelle with
- dynamic @{setting PATH} lookup etc., although it might fail if a
- different version of Proof General is already part of the Emacs
- installation of the operating system.
-
- The actual interface script is part of the Proof General
- distribution; its usage depends on the particular version. There
- are some options available, such as @{verbatim "-l"} for passing the
- logic image to be used by default, or @{verbatim "-m"} to tune the
- standard print mode of the prover process. The following Isabelle
- settings are particularly important for Proof General:
-
- \begin{description}
-
- \item[@{setting_def PROOFGENERAL_HOME}] points to the main
- installation directory of the Proof General distribution. This is
- implicitly provided for versions of Proof General that are
- distributed as Isabelle component, see also \secref{sec:components};
- otherwise it needs to be configured manually.
-
- \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
- the command line of any invocation of the Proof General @{verbatim
- interface} script. This allows to provide persistent default
- options for the invocation of \texttt{isabelle emacs}.
-
- \end{description}
-*}
-
-
-section {* Plain TTY interaction \label{sec:tool-tty} *}
-
-text {*
- The @{tool_def tty} tool runs the Isabelle process interactively
- within a plain terminal session:
-\begin{ttbox}
-Usage: isabelle tty [OPTIONS]
-
- Options are:
- -l NAME logic image name (default ISABELLE_LOGIC)
- -m MODE add print mode for output
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -p NAME line editor program name (default ISABELLE_LINE_EDITOR)
-
- Run Isabelle process with plain tty interaction and line editor.
-\end{ttbox}
-
- The @{verbatim "-l"} option specifies the logic image. The
- @{verbatim "-m"} option specifies additional print modes. The
- @{verbatim "-p"} option specifies an alternative line editor (such
- as the @{executable_def rlwrap} wrapper for GNU readline); the
- fall-back is to use raw standard input.
-
- \medskip Option @{verbatim "-o"} allows to override Isabelle system
- options for this process, see also \secref{sec:system-options}.
-
- Regular interaction works via the standard Isabelle/Isar toplevel
- loop. The Isar command @{command exit} drops out into the
- bare-bones ML system, which is occasionally useful for debugging of
- the Isar 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. *}
-
-
-subsection {* Invoking the graph browser *}
-
-text {* The stand-alone version of the graph browser is wrapped up as
- @{tool_def browser}:
-\begin{ttbox}
-Usage: isabelle 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 file name 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/src/Doc/System/Misc.thy Mon Jun 16 12:41:51 2014 +0200
+++ b/src/Doc/System/Misc.thy Mon Jun 16 12:52:20 2014 +0200
@@ -10,6 +10,176 @@
*}
+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. *}
+
+
+subsection {* Invoking the graph browser *}
+
+text {* The stand-alone version of the graph browser is wrapped up as
+ @{tool_def browser}:
+\begin{ttbox}
+Usage: isabelle 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 file name 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 {* Resolving Isabelle components \label{sec:tool-components} *}
text {*
@@ -98,6 +268,41 @@
*}
+section {* Proof General / Emacs *}
+
+text {* The @{tool_def emacs} tool invokes a version of Emacs and
+ Proof General\footnote{@{url "http://proofgeneral.inf.ed.ac.uk/"}} within the
+ regular Isabelle settings environment (\secref{sec:settings}). This
+ is more convenient than starting Emacs separately, loading the Proof
+ General LISP files, and then attempting to start Isabelle with
+ dynamic @{setting PATH} lookup etc., although it might fail if a
+ different version of Proof General is already part of the Emacs
+ installation of the operating system.
+
+ The actual interface script is part of the Proof General
+ distribution; its usage depends on the particular version. There
+ are some options available, such as @{verbatim "-l"} for passing the
+ logic image to be used by default, or @{verbatim "-m"} to tune the
+ standard print mode of the prover process. The following Isabelle
+ settings are particularly important for Proof General:
+
+ \begin{description}
+
+ \item[@{setting_def PROOFGENERAL_HOME}] points to the main
+ installation directory of the Proof General distribution. This is
+ implicitly provided for versions of Proof General that are
+ distributed as Isabelle component, see also \secref{sec:components};
+ otherwise it needs to be configured manually.
+
+ \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
+ the command line of any invocation of the Proof General @{verbatim
+ interface} script. This allows to provide persistent default
+ options for the invocation of \texttt{isabelle emacs}.
+
+ \end{description}
+*}
+
+
section {* Shell commands within the settings environment \label{sec:tool-env} *}
text {* The @{tool_def env} tool is a direct wrapper for the standard
@@ -234,6 +439,39 @@
using this template. *}
+section {* Plain TTY interaction \label{sec:tool-tty} *}
+
+text {*
+ The @{tool_def tty} tool runs the Isabelle process interactively
+ within a plain terminal session:
+\begin{ttbox}
+Usage: isabelle tty [OPTIONS]
+
+ Options are:
+ -l NAME logic image name (default ISABELLE_LOGIC)
+ -m MODE add print mode for output
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -p NAME line editor program name (default ISABELLE_LINE_EDITOR)
+
+ Run Isabelle process with plain tty interaction and line editor.
+\end{ttbox}
+
+ The @{verbatim "-l"} option specifies the logic image. The
+ @{verbatim "-m"} option specifies additional print modes. The
+ @{verbatim "-p"} option specifies an alternative line editor (such
+ as the @{executable_def rlwrap} wrapper for GNU readline); the
+ fall-back is to use raw standard input.
+
+ \medskip Option @{verbatim "-o"} allows to override Isabelle system
+ options for this process, see also \secref{sec:system-options}.
+
+ Regular interaction works via the standard Isabelle/Isar toplevel
+ loop. The Isar command @{command exit} drops out into the
+ bare-bones ML system, which is occasionally useful for debugging of
+ the Isar infrastructure itself. Invoking @{ML Isar.loop}~@{verbatim
+ "();"} in ML will return to the Isar toplevel. *}
+
+
section {* Remove awkward symbol names from theory sources *}
text {*
--- a/src/Doc/System/document/root.tex Mon Jun 16 12:41:51 2014 +0200
+++ b/src/Doc/System/document/root.tex Mon Jun 16 12:52:20 2014 +0200
@@ -30,7 +30,6 @@
\pagenumbering{roman} \tableofcontents \clearfirst
\input{Basics.tex}
-\input{Interfaces.tex}
\input{Sessions.tex}
\input{Presentation.tex}
\input{Scala.tex}