# HG changeset patch
# User wenzelm
# Date 975695994 -3600
# Node ID fcd29e58c40cdcb8ba738688bf2ad7a47fb8d7c5
# Parent  d960cc4a6afcb678d99bd98dc536bf4f9df6ea5b
option -m;

diff -r d960cc4a6afc -r fcd29e58c40c lib/Tools/usedir
--- a/lib/Tools/usedir	Fri Dec 01 13:47:37 2000 +0100
+++ b/lib/Tools/usedir	Fri Dec 01 19:39:54 2000 +0100
@@ -22,8 +22,8 @@
   echo "    -b           build mode (output heap image, using current dir)"
   echo "    -c BOOL      tell ML system to compress output image (default true)"
   echo "    -d FORMAT    build document as FORMAT (default false)"
-  echo "    -i BOOL      generate theory browsing information,"
-  echo "                 i.e. HTML / graph data (default false)"
+  echo "    -i BOOL      generate theory browser information (default false)"
+  echo "    -m MODE      add print mode for output"
   echo "    -r           reset session path"
   echo "    -s NAME      override session NAME"
   echo
@@ -46,13 +46,14 @@
 COMPRESS=true
 DOCUMENT=false
 INFO=false
+MODES=""
 RESET=false
 SESSION=""
 
 function getoptions()
 {
   OPTIND=1
-  while getopts "D:P:bc:d:i:rs:" OPT
+  while getopts "D:P:bc:d:i:m:rs:" OPT
   do
     case "$OPT" in
       D)
@@ -73,6 +74,13 @@
       i)
         INFO="$OPTARG"
         ;;
+      m)
+        if [ -z "$MODES" ]; then
+          MODES="\"$OPTARG\""
+        else
+          MODES="$MODES, \"$OPTARG\""
+        fi
+        ;;
       r)
         RESET=true
         ;;
@@ -145,7 +153,7 @@
   [ "$COMPRESS" = true ] && OPT_C="-c"
 
   "$ISABELLE" \
-    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \
+    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \
     $OPT_C -q -w $LOGIC $NAME > "$LOG" 2>&1
   RC="$?"
 else
@@ -154,7 +162,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE" \
-    -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\"; quit();" \
+    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\"; quit();" \
     -r -q "$LOGIC" > "$LOG" 2>&1
   RC="$?"
   cd ..