# HG changeset patch
# User wenzelm
# Date 1267820781 -3600
# Node ID f037aa6699c37d0b98c1fb90ea146064de065a4c
# Parent  f57de4a9eb9c43fdb18dd1f97f44e24066483947
isabelle browser -b: Admin/build only;

diff -r f57de4a9eb9c -r f037aa6699c3 doc-src/System/Thy/Presentation.thy
--- a/doc-src/System/Thy/Presentation.thy	Fri Mar 05 09:27:47 2010 -0800
+++ b/doc-src/System/Thy/Presentation.thy	Fri Mar 05 21:26:21 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 f57de4a9eb9c -r f037aa6699c3 doc-src/System/Thy/document/Presentation.tex
--- a/doc-src/System/Thy/document/Presentation.tex	Fri Mar 05 09:27:47 2010 -0800
+++ b/doc-src/System/Thy/document/Presentation.tex	Fri Mar 05 21:26:21 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 f57de4a9eb9c -r f037aa6699c3 lib/Tools/browser
--- a/lib/Tools/browser	Fri Mar 05 09:27:47 2010 -0800
+++ b/lib/Tools/browser	Fri Mar 05 21:26:21 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"