--- a/src/Doc/ROOT Thu Dec 31 15:27:25 2015 +0100
+++ b/src/Doc/ROOT Thu Dec 31 19:53:19 2015 +0100
@@ -370,7 +370,6 @@
document_files (in "../Isar_Ref/document")
"style.sty"
document_files
- "browser_screenshot.png"
"build"
"root.tex"
--- a/src/Doc/System/Basics.thy Thu Dec 31 15:27:25 2015 +0100
+++ b/src/Doc/System/Basics.thy Thu Dec 31 19:53:19 2015 +0100
@@ -35,15 +35,15 @@
section \<open>Isabelle settings \label{sec:settings}\<close>
text \<open>
- The Isabelle system heavily depends on the \<^emph>\<open>settings
- mechanism\<close>\indexbold{settings}. Essentially, this is a statically scoped
- collection of environment variables, such as @{setting ISABELLE_HOME},
- @{setting ML_SYSTEM}, @{setting ML_HOME}. These variables are \<^emph>\<open>not\<close>
- intended to be set directly from the shell, though. Isabelle employs a
- somewhat more sophisticated scheme of \<^emph>\<open>settings files\<close> --- one for
- site-wide defaults, another for additional user-specific modifications. With
- all configuration variables in clearly defined places, this scheme is more
- maintainable and user-friendly than global shell environment variables.
+ The Isabelle system heavily depends on the \<^emph>\<open>settings mechanism\<close>.
+ Essentially, this is a statically scoped collection of environment
+ variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting
+ ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the
+ shell, though. Isabelle employs a somewhat more sophisticated scheme of
+ \<^emph>\<open>settings files\<close> --- one for site-wide defaults, another for additional
+ user-specific modifications. With all configuration variables in clearly
+ defined places, this scheme is more maintainable and user-friendly than
+ global shell environment variables.
In particular, we avoid the typical situation where prospective users of a
software package are told to put several things into their shell startup
@@ -209,9 +209,8 @@
is appended here, too.
\<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
- browser information (HTML text, graph data, and printable documents) is
- stored (see also \secref{sec:info}). The default value is @{file_unchecked
- "$ISABELLE_HOME_USER/browser_info"}.
+ browser information is stored as HTML and PDF (see also \secref{sec:info}).
+ The default value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
\<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
--- a/src/Doc/System/Misc.thy Thu Dec 31 15:27:25 2015 +0100
+++ b/src/Doc/System/Misc.thy Thu Dec 31 19:53:19 2015 +0100
@@ -12,155 +12,6 @@
\<close>
-section \<open>Theory graph browser \label{sec:browse}\<close>
-
-text \<open>
- 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.
-\<close>
-
-
-subsection \<open>Invoking the graph browser\<close>
-
-text \<open>
- The stand-alone version of the graph browser is wrapped up as @{tool_def
- browser}:
- @{verbatim [display]
-\<open>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)\<close>}
-
- When no file name is specified, the browser automatically changes to the
- directory @{setting ISABELLE_BROWSER_INFO}.
-
- \<^medskip>
- The \<^verbatim>\<open>-b\<close> option indicates that this is for administrative build only, i.e.\
- no browser popup if no files are given.
-
- The \<^verbatim>\<open>-c\<close> option causes the input file to be removed after use.
-
- The \<^verbatim>\<open>-o\<close> option indicates batch-mode operation, with the output written to
- the indicated file; note that \<^verbatim>\<open>pdf\<close> produces an \<^verbatim>\<open>eps\<close> 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.
-\<close>
-
-
-subsection \<open>Using the graph browser\<close>
-
-text \<open>
- 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}
-\<close>
-
-
-subsubsection \<open>The directory tree window\<close>
-
-text \<open>
- We describe the usage of the directory browser and the meaning of the
- different items in the browser window.
-
- \<^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.
-\<close>
-
-
-subsubsection \<open>The graph display window\<close>
-
-text \<open>
- 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>\<open>[....]\<close>''. To uncollapse the nodes again,
- simply click on the red arrow or on the node with the name ``\<^verbatim>\<open>[....]\<close>''.
- Similar to the directory browser, the contents of theory files can be
- displayed by double clicking on the corresponding node.
-\<close>
-
-
-subsubsection \<open>The ``File'' menu\<close>
-
-text \<open>
- 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:
-
- \<^descr>[Open \dots] Open a new graph file.
-
- \<^descr>[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.
-
- \<^descr>[Export to EPS] Outputs the current graph in Encapsulated Postscript
- format. The resulting file can be included in other documents.
-
- \<^descr>[Quit] Quit the graph browser.
-\<close>
-
-
-subsection \<open>Syntax of graph definition files\<close>
-
-text \<open>
- A graph definition file has the following syntax:
-
- \begin{center}\small
- \begin{tabular}{rcl}
- \<open>graph\<close> & \<open>=\<close> & \<open>{ vertex\<close>~\<^verbatim>\<open>;\<close>~\<open>}+\<close> \\
- \<open>vertex\<close> & \<open>=\<close> & \<open>vertex_name vertex_ID dir_name [\<close>~\<^verbatim>\<open>+\<close>~\<open>] path [\<close>~\<^verbatim>\<open><\<close>~\<open>|\<close>~\<^verbatim>\<open>>\<close>~\<open>] { vertex_ID }*\<close>
- \end{tabular}
- \end{center}
-
- The meaning of the items in a vertex description is as follows:
-
- \<^descr>[\<open>vertex_name\<close>] The name of the vertex.
-
- \<^descr>[\<open>vertex_ID\<close>] The vertex identifier. Note that there may be several
- vertices with equal names, whereas identifiers must be unique.
-
- \<^descr>[\<open>dir_name\<close>] The name of the ``directory'' the vertex should be placed in.
- A ``\<^verbatim>\<open>+\<close>'' sign after \<open>dir_name\<close> indicates that the nodes in the directory
- are initially visible. Directories are initially invisible by default.
-
- \<^descr>[\<open>path\<close>] The path of the corresponding theory file. This is specified
- relatively to the path of the graph definition file.
-
- \<^descr>[List of successor/predecessor nodes] A ``\<^verbatim>\<open><\<close>'' sign before the list means
- that successor nodes are listed, a ``\<^verbatim>\<open>>\<close>'' sign means that predecessor
- nodes are listed. If neither ``\<^verbatim>\<open><\<close>'' nor ``\<^verbatim>\<open>>\<close>'' is found, the browser
- assumes that successor nodes are listed.
-\<close>
-
-
section \<open>Resolving Isabelle components \label{sec:tool-components}\<close>
text \<open>
--- a/src/Doc/System/Presentation.thy Thu Dec 31 15:27:25 2015 +0100
+++ b/src/Doc/System/Presentation.thy Thu Dec 31 19:53:19 2015 +0100
@@ -51,11 +51,9 @@
\<close>
-section \<open>Generating theory browser information \label{sec:info}\<close>
+section \<open>Generating HTML browser information \label{sec:info}\<close>
text \<open>
- \index{theory browsing information|bold}
-
As a side-effect of building sessions, Isabelle is able to generate theory
browsing information, including HTML documents that show the theory sources
and the relationship with its ancestors and descendants. Besides the HTML
@@ -65,24 +63,16 @@
implicit tree structure of the session build hierarchy is \<^emph>\<open>not\<close> relevant
for the presentation.
- Isabelle also generates graph files that represent the theory dependencies
- within a session. There is a graph browser Java applet embedded in the
- generated HTML pages, and also a stand-alone application that allows
- browsing theory graphs without having to start a WWW client first. The
- latter version also includes features such as generating Postscript files,
- which are not available in the applet version. See \secref{sec:browse} for
- further information.
-
\<^medskip>
- The easiest way to let Isabelle generate theory browsing information for
- existing sessions is to invoke @{tool build} with suitable options:
+ To generate theory browsing information for an existing session, just invoke
+ @{tool build} with suitable options:
@{verbatim [display] \<open>isabelle build -o browser_info -v -c FOL\<close>}
The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as
reported by the above verbose invocation of the build process.
Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in @{file
- "~~/src/HOL/Library"}) also provide actual printable documents. These are
+ "~~/src/HOL/Library"}) also provide printable documents in PDF. These are
prepared automatically as well if enabled like this:
@{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
Binary file src/Doc/System/document/browser_screenshot.png has changed
--- a/src/Doc/System/document/root.tex Thu Dec 31 15:27:25 2015 +0100
+++ b/src/Doc/System/document/root.tex Thu Dec 31 19:53:19 2015 +0100
@@ -20,8 +20,7 @@
\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}
-\author{\emph{Makarius Wenzel} and \emph{Stefan Berghofer} \\
- TU M\"unchen}
+\author{\emph{Makarius Wenzel}}
\makeindex
--- a/src/Doc/manual.bib Thu Dec 31 15:27:25 2015 +0100
+++ b/src/Doc/manual.bib Thu Dec 31 19:53:19 2015 +0100
@@ -1908,28 +1908,24 @@
note = {\url{http://www.spass-prover.org/publications/spass.pdf}}}
@manual{isabelle-system,
- author = {Makarius Wenzel and Stefan Berghofer},
- title = {The {Isabelle} System Manual},
- institution = {TU Munich},
- note = {\url{http://isabelle.in.tum.de/doc/system.pdf}}}
+ author = {Makarius Wenzel},
+ title = {The {Isabelle} System Manual},
+ note = {\url{http://isabelle.in.tum.de/doc/system.pdf}}}
@manual{isabelle-jedit,
- author = {Makarius Wenzel},
- title = {{Isabelle/jEdit}},
- institution = {TU Munich},
- note = {\url{http://isabelle.in.tum.de/doc/jedit.pdf}}}
+ author = {Makarius Wenzel},
+ title = {{Isabelle/jEdit}},
+ note = {\url{http://isabelle.in.tum.de/doc/jedit.pdf}}}
@manual{isabelle-isar-ref,
- author = {Makarius Wenzel},
- title = {The {Isabelle/Isar} Reference Manual},
- institution = {TU Munich},
- note = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
+ author = {Makarius Wenzel},
+ title = {The {Isabelle/Isar} Reference Manual},
+ note = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
@manual{isabelle-implementation,
- author = {Makarius Wenzel},
- title = {The {Isabelle/Isar} Implementation},
- institution = {TU Munich},
- note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
+ author = {Makarius Wenzel},
+ title = {The {Isabelle/Isar} Implementation},
+ note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
@InProceedings{Wenzel:1999:TPHOL,
author = {Markus Wenzel},
