--- a/lib/Tools/usedir Wed Mar 08 17:36:54 2000 +0100
+++ b/lib/Tools/usedir Wed Mar 08 17:39:08 2000 +0100
@@ -18,6 +18,7 @@
echo " -D PATH dump generated document sources into PATH"
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)"
echo " -d FORMAT build document as FORMAT (default false)"
echo " -i BOOL generate theory browsing information,"
echo " i.e. HTML / graph data (default false)"
@@ -40,6 +41,7 @@
DUMP=""
RPATH=""
BUILD=""
+COMPRESS=""
DOCUMENT=false
INFO=false
RESET=false
@@ -60,6 +62,9 @@
b)
BUILD=true
;;
+ c)
+ COMPRESS="$OPTARG"
+ ;;
d)
DOCUMENT="$OPTARG"
;;
@@ -139,9 +144,12 @@
echo "Building $ITEM ..."
LOG="$LOGDIR/$ITEM"
+ OPT_C=""
+ [ "$COMPRESS" = true ] && OPT_C="-c"
+
$ISABELLE \
-e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \
- -q -w $LOGIC $NAME > $LOG 2>&1
+ $OPT_C -q -w $LOGIC $NAME > $LOG 2>&1
RC=$?
else
ITEM=$(basename $LOGIC)-"$SESSION"