option -c: tell ML system to compress output image;
authorwenzelm
Wed Mar 08 17:39:08 2000 +0100 (2000-03-08)
changeset 8359124ad46105dd
parent 8358 a57d72b5d272
child 8360 885a6414b9c8
option -c: tell ML system to compress output image;
bin/isabelle
lib/Tools/usedir
     1.1 --- a/bin/isabelle	Wed Mar 08 17:36:54 2000 +0100
     1.2 +++ b/bin/isabelle	Wed Mar 08 17:39:08 2000 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4    echo
     1.5    echo "  Options are:"
     1.6    echo "    -I           startup Isar interaction mode"
     1.7 +  echo "    -c           tell ML system to compress output image"
     1.8    echo "    -e MLTEXT    pass MLTEXT to the ML session"
     1.9    echo "    -m MODE      add print mode for output"
    1.10    echo "    -q           non-interactive session"
    1.11 @@ -49,18 +50,22 @@
    1.12  
    1.13  # options
    1.14  
    1.15 +COMPRESS=""
    1.16  MLTEXT=""
    1.17  MODES=""
    1.18  TERMINATE=""
    1.19  READONLY=""
    1.20  NOWRITE=""
    1.21  
    1.22 -while getopts "Ie:m:qruw" OPT
    1.23 +while getopts "Ice:m:qruw" OPT
    1.24  do
    1.25    case "$OPT" in
    1.26      I)
    1.27        MLTEXT="$MLTEXT Isar.main();"
    1.28        ;;
    1.29 +    c)
    1.30 +      COMPRESS=true
    1.31 +      ;;
    1.32      e)
    1.33        MLTEXT="$MLTEXT $OPTARG"
    1.34        ;;
    1.35 @@ -177,7 +182,7 @@
    1.36  
    1.37  [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
    1.38  
    1.39 -export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP
    1.40 +export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
    1.41  
    1.42  if [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ]; then
    1.43    $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
     2.1 --- a/lib/Tools/usedir	Wed Mar 08 17:36:54 2000 +0100
     2.2 +++ b/lib/Tools/usedir	Wed Mar 08 17:39:08 2000 +0100
     2.3 @@ -18,6 +18,7 @@
     2.4    echo "    -D PATH      dump generated document sources into PATH"
     2.5    echo "    -P PATH      set path for remote theory browsing information"
     2.6    echo "    -b           build mode (output heap image, using current dir)"
     2.7 +  echo "    -c BOOL      tell ML system to compress output image (default true)"
     2.8    echo "    -d FORMAT    build document as FORMAT (default false)"
     2.9    echo "    -i BOOL      generate theory browsing information,"
    2.10    echo "                 i.e. HTML / graph data (default false)"
    2.11 @@ -40,6 +41,7 @@
    2.12  DUMP=""
    2.13  RPATH=""
    2.14  BUILD=""
    2.15 +COMPRESS=""
    2.16  DOCUMENT=false
    2.17  INFO=false
    2.18  RESET=false
    2.19 @@ -60,6 +62,9 @@
    2.20        b)
    2.21          BUILD=true
    2.22          ;;
    2.23 +      c)
    2.24 +        COMPRESS="$OPTARG"
    2.25 +        ;;
    2.26        d)
    2.27          DOCUMENT="$OPTARG"
    2.28          ;;
    2.29 @@ -139,9 +144,12 @@
    2.30    echo "Building $ITEM ..."
    2.31    LOG="$LOGDIR/$ITEM"
    2.32  
    2.33 +  OPT_C=""
    2.34 +  [ "$COMPRESS" = true ] && OPT_C="-c"
    2.35 +
    2.36    $ISABELLE \
    2.37      -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \
    2.38 -    -q -w $LOGIC $NAME > $LOG 2>&1
    2.39 +    $OPT_C -q -w $LOGIC $NAME > $LOG 2>&1
    2.40    RC=$?
    2.41  else
    2.42    ITEM=$(basename $LOGIC)-"$SESSION"