Added new option for setting level of detail for proof objects.
--- 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 ..