lib/Tools/usedir

   echo
   echo "  Options are:"
   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)"
   echo "    -r           reset session path"
   echo "    -s NAME      override session NAME"

 # options
 
 DUMP=""
 RPATH=""
 BUILD=""
+COMPRESS=""
 DOCUMENT=false
 INFO=false
 RESET=false
 SESSION=""
 

       P)
         RPATH="$OPTARG"
         ;;
       b)
         BUILD=true
+        ;;
+      c)
+        COMPRESS="$OPTARG"
         ;;
       d)
         DOCUMENT="$OPTARG"
         ;;
       i)

 if [ -n "$BUILD" ]; then
   ITEM="$SESSION"
   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"
   echo "Running $ITEM ..."
   LOG="$LOGDIR/$ITEM"