# HG changeset patch
# User wenzelm
# Date 1267828318 -3600
# Node ID ad7d2f9cc47dfcd4387adeda8f058960b9a8e235
# Parent  f1429d5df3d2381c63fd07594f2ab4633be4a7af# Parent  f638444c966793b318be5151b967dfe1ca4c8ed2
merged

diff -r f638444c9667 -r ad7d2f9cc47d doc-src/System/Thy/Presentation.thy
--- 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}
diff -r f638444c9667 -r ad7d2f9cc47d doc-src/System/Thy/document/Presentation.tex
--- 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|
diff -r f638444c9667 -r ad7d2f9cc47d lib/Tools/browser
--- 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"
diff -r f638444c9667 -r ad7d2f9cc47d src/Pure/Thy/present.ML
--- 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));