diff -r cb5bfb32ab39 -r ee392b6181a4 lib/Tools/usedir --- a/lib/Tools/usedir Tue Jan 11 14:18:06 2005 +0100 +++ b/lib/Tools/usedir Tue Jan 11 14:19:08 2005 +0100 @@ -17,6 +17,7 @@ echo echo " Options are:" echo " -D PATH dump generated document sources into PATH" + echo " -H BOOL hide proofs and some other commands in document (default false)" echo " -P PATH set path for remote theory browsing information" echo " -b build mode (output heap image, using current dir)" echo " -c BOOL tell ML system to compress output image (default true)" @@ -64,6 +65,7 @@ BUILD="" COMPRESS=true DOCUMENT=false +HIDE=false ROOT_FILE=ROOT.ML DOCUMENT_GRAPH=false INFO=false @@ -76,12 +78,16 @@ function getoptions() { OPTIND=1 - while getopts "D:P:bc:d:f:g:i:m:p:rs:v:" OPT + while getopts "D:H:P:bc:d:f:g:i:m:p:rs:v:" OPT do case "$OPT" in D) DUMP="$OPTARG" ;; + H) + check_bool "$OPTARG" + HIDE="$OPTARG" + ;; P) RPATH="$OPTARG" ;; @@ -194,7 +200,7 @@ [ "$COMPRESS" = true ] && OPT_C="-c" "$ISABELLE" \ - -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE;" \ + -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE $HIDE;" \ $OPT_C -q -w $LOGIC $NAME > "$LOG" RC="$?" else @@ -203,7 +209,7 @@ LOG="$LOGDIR/$ITEM" "$ISABELLE" \ - -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE; quit();" \ + -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE $HIDE; quit();" \ -r -q "$LOGIC" > "$LOG" RC="$?" cd ..