# HG changeset patch
# User berghofe
# Date 999268231 -7200
# Node ID 7f4c5cdea239c5104ce043c037263820bc1b5365
# Parent  0494d0347f18d57fe48eac64ec24a81364d5129d
Added new option for setting level of detail for proof objects.

diff -r 0494d0347f18 -r 7f4c5cdea239 lib/Tools/usedir
--- a/lib/Tools/usedir	Fri Aug 31 16:29:18 2001 +0200
+++ b/lib/Tools/usedir	Fri Aug 31 16:30:31 2001 +0200
@@ -24,6 +24,7 @@
   echo "    -d FORMAT    build document as FORMAT (default false)"
   echo "    -i BOOL      generate theory browser information (default false)"
   echo "    -m MODE      add print mode for output"
+  echo "    -p LEVEL     set level of detail for proof objects"
   echo "    -r           reset session path"
   echo "    -s NAME      override session NAME"
   echo
@@ -49,11 +50,12 @@
 MODES=""
 RESET=false
 SESSION=""
+PROOF=MinDeriv
 
 function getoptions()
 {
   OPTIND=1
-  while getopts "D:P:bc:d:i:m:rs:" OPT
+  while getopts "D:P:bc:d:i:m:p:rs:" OPT
   do
     case "$OPT" in
       D)
@@ -81,6 +83,9 @@
           MODES="\"$OPTARG\", $MODES"
         fi
         ;;
+      p)
+        PROOF="$OPTARG"
+        ;;
       r)
         RESET=true
         ;;
@@ -153,7 +158,7 @@
   [ "$COMPRESS" = true ] && OPT_C="-c"
 
   "$ISABELLE" \
-    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \
+    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOF;" \
     $OPT_C -q -w $LOGIC $NAME > "$LOG" 2>&1
   RC="$?"
 else
@@ -162,7 +167,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE" \
-    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\"; quit();" \
+    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOF; quit();" \
     -r -q "$LOGIC" > "$LOG" 2>&1
   RC="$?"
   cd ..