# HG changeset patch
# User wenzelm
# Date 952533548 -3600
# Node ID 124ad46105dd30ba77157e7fc2c70def83e5e1da
# Parent  a57d72b5d272e467b4dec4350c2448f3fead83ab
option -c: tell ML system to compress output image;

diff -r a57d72b5d272 -r 124ad46105dd bin/isabelle
--- a/bin/isabelle	Wed Mar 08 17:36:54 2000 +0100
+++ b/bin/isabelle	Wed Mar 08 17:39:08 2000 +0100
@@ -23,6 +23,7 @@
   echo
   echo "  Options are:"
   echo "    -I           startup Isar interaction mode"
+  echo "    -c           tell ML system to compress output image"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
   echo "    -m MODE      add print mode for output"
   echo "    -q           non-interactive session"
@@ -49,18 +50,22 @@
 
 # options
 
+COMPRESS=""
 MLTEXT=""
 MODES=""
 TERMINATE=""
 READONLY=""
 NOWRITE=""
 
-while getopts "Ie:m:qruw" OPT
+while getopts "Ice:m:qruw" OPT
 do
   case "$OPT" in
     I)
       MLTEXT="$MLTEXT Isar.main();"
       ;;
+    c)
+      COMPRESS=true
+      ;;
     e)
       MLTEXT="$MLTEXT $OPTARG"
       ;;
@@ -177,7 +182,7 @@
 
 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
 
-export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP
+export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
 
 if [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ]; then
   $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
diff -r a57d72b5d272 -r 124ad46105dd lib/Tools/usedir
--- 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"