# 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 ..