# HG changeset patch
# User berghofe
# Date 875616735 -7200
# Node ID cd9b6c86926c5e2afb41ca8cd94e2d35959bb0ce
# Parent  e832a36121abc73a4f75794a1624f6c261ed374d
There is now one single option -i for generating theory browsing
information instead of the two options -h and -g .

diff -r e832a36121ab -r cd9b6c86926c lib/Tools/usedir
--- a/lib/Tools/usedir	Tue Sep 30 12:49:16 1997 +0200
+++ b/lib/Tools/usedir	Tue Sep 30 12:52:15 1997 +0200
@@ -16,8 +16,8 @@
   echo
   echo "  Options are:"
   echo "    -b           build mode (output heap image, use dir \".\")"
-  echo "    -g BOOL      generate theory graph data (default false)"
-  echo "    -h BOOL      generate theory HTML data (default false)"
+  echo "    -i BOOL      generate theory browsing information,"
+  echo "                 i.e. HTML / graph data (default false)"
   echo "    -s NAME      override session NAME"
   echo
   echo "  Build object-logic or run examples. Also creates browsing"
@@ -32,24 +32,20 @@
 # options
 
 BUILD=""
-GRAPH=false
-HTML=false
+INFO=false
 SESSION=""
 
 function getoptions()
 {
   OPTIND=1
-  while getopts "bcg:h:s:" OPT
+  while getopts "bi:s:" OPT
   do
     case "$OPT" in
       b)
         BUILD=true
         ;;
-      g)
-        GRAPH="$OPTARG"
-        ;;
-      h)
-        HTML="$OPTARG"
+      i)
+        INFO="$OPTARG"
         ;;
       s)
         SESSION="$OPTARG"
@@ -77,19 +73,10 @@
 
 # prepare directories for html and graph output
 
-if [ $HTML = "true" -o $GRAPH = "true" ]; then
-  if [ ! -d $ISABELLE_BROWSER_INFO/gif ]; then
-    mkdir -p $ISABELLE_BROWSER_INFO/gif
-    cp $ISABELLE_HOME/lib/images/*.gif $ISABELLE_BROWSER_INFO/gif
-  fi
-fi
-
-if [ $HTML = "true" -a ! -d $ISABELLE_BROWSER_INFO/html ]; then
-  mkdir -p $ISABELLE_BROWSER_INFO/html
-  cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/html/index.html
-fi
-
-if [ $GRAPH = "true" -a ! -d $ISABELLE_BROWSER_INFO/graph ]; then
+if [ $INFO = "true" -a ! -d $ISABELLE_BROWSER_INFO ]; then
+  mkdir -p $ISABELLE_BROWSER_INFO/gif
+  cp $ISABELLE_HOME/lib/images/*.gif $ISABELLE_BROWSER_INFO/gif
+  cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html
   mkdir -p $ISABELLE_BROWSER_INFO/graph
   cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html
   mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
@@ -105,10 +92,10 @@
 
 if [ -n "$BUILD" ]; then
   exec $ISABELLE \
-    -e "make_html := $HTML; make_graph := $GRAPH; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \
+    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \
     -q -w $LOGIC $NAME
 else
   exec $ISABELLE \
-    -e "make_html := $HTML; make_graph := $GRAPH; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \
+    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \
     -r -q $LOGIC
 fi