--- a/doc-src/System/Thy/Presentation.thy Fri Mar 05 13:33:17 2010 -0800
+++ b/doc-src/System/Thy/Presentation.thy Fri Mar 05 23:31:58 2010 +0100
@@ -183,14 +183,19 @@
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 "-c"} option causes the input file to be
- removed after use.
+ \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}
--- a/doc-src/System/Thy/document/Presentation.tex Fri Mar 05 13:33:17 2010 -0800
+++ b/doc-src/System/Thy/document/Presentation.tex Fri Mar 05 23:31:58 2010 +0100
@@ -198,14 +198,19 @@
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{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}.
- \medskip The \verb|-c| option causes the input file to be
- removed after use.
+ \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|
--- a/lib/Tools/browser Fri Mar 05 13:33:17 2010 -0800
+++ b/lib/Tools/browser Fri Mar 05 23:31:58 2010 +0100
@@ -13,6 +13,7 @@
echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]"
echo
echo " Options are:"
+ echo " -b Admin/build only"
echo " -c cleanup -- remove GRAPHFILE after use"
echo " -o FILE output to FILE (ps, eps, pdf)"
echo
@@ -30,12 +31,16 @@
# options
+ADMIN_BUILD=""
CLEAN=""
OUTFILE=""
-while getopts "co:" OPT
+while getopts "bco:" OPT
do
case "$OPT" in
+ b)
+ ADMIN_BUILD=true
+ ;;
c)
CLEAN=true
;;
@@ -64,10 +69,7 @@
classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
-if [ -z "$GRAPHFILE" ]; then
- [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
- exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
-else
+if [ -n "$GRAPHFILE" ]; then
PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
if [ -n "$CLEAN" ]; then
mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
@@ -95,6 +97,11 @@
fi
rm -f "$PRIVATE_FILE"
+elif [ -z "$ADMIN_BUILD" ]; then
+ [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
+ exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
+else
+ RC=0
fi
exit "$RC"
--- a/src/Pure/Thy/present.ML Fri Mar 05 13:33:17 2010 -0800
+++ b/src/Pure/Thy/present.ML Fri Mar 05 23:31:58 2010 +0100
@@ -402,6 +402,7 @@
if length path > 1 then update_index parent_html_prefix name else ();
(case readme of NONE => () | SOME path => File.copy path html_prefix);
write_graph sorted_graph (Path.append html_prefix graph_path);
+ File.isabelle_tool "browser" "-b";
File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
(HTML.applet_pages name (Url.File index_path, name));