# HG changeset patch
# User wenzelm
# Date 1243777775 -7200
# Node ID 1f5740424c69e7a84bc9568b89e409999ab7aaf1
# Parent  39fe8093b1dfda2ec2ab52a084f8c778a3e7efb0
removed "compress" option from isabelle-process and isabelle usedir -- this is always enabled;

diff -r 39fe8093b1df -r 1f5740424c69 NEWS
--- a/NEWS	Sun May 31 15:29:43 2009 +0200
+++ b/NEWS	Sun May 31 15:49:35 2009 +0200
@@ -37,6 +37,9 @@
 
 * Discontinued support for Poly/ML 4.x versions.
 
+* Removed "compress" option from isabelle-process and isabelle usedir;
+this is always enabled.
+
 
 
 New in Isabelle2009 (April 2009)
diff -r 39fe8093b1df -r 1f5740424c69 bin/isabelle-process
--- a/bin/isabelle-process	Sun May 31 15:29:43 2009 +0200
+++ b/bin/isabelle-process	Sun May 31 15:49:35 2009 +0200
@@ -31,7 +31,6 @@
   echo "    -S           secure mode -- disallow critical operations"
   echo "    -X           startup PGIP interaction mode"
   echo "    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream"
-  echo "    -c           tell ML system to compress output image"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
   echo "    -f           pass 'Session.finish();' to the ML session"
   echo "    -m MODE      add print mode for output"
@@ -64,14 +63,13 @@
 SECURE=""
 WRAPPER_OUTPUT=""
 PGIP=""
-COMPRESS=""
 MLTEXT=""
 MODES=""
 TERMINATE=""
 READONLY=""
 NOWRITE=""
 
-while getopts "IPSW:Xce:fm:qruw" OPT
+while getopts "IPSW:Xe:fm:qruw" OPT
 do
   case "$OPT" in
     I)
@@ -89,9 +87,6 @@
     X)
       PGIP=true
       ;;
-    c)
-      COMPRESS=true
-      ;;
     e)
       MLTEXT="$MLTEXT $OPTARG"
       ;;
@@ -230,7 +225,7 @@
   NICE=""
 fi
 
-export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP
+export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP
 
 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
diff -r 39fe8093b1df -r 1f5740424c69 doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Sun May 31 15:29:43 2009 +0200
+++ b/doc-src/System/Thy/Basics.thy	Sun May 31 15:49:35 2009 +0200
@@ -271,7 +271,6 @@
     -S           secure mode -- disallow critical operations
     -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream
     -X           startup PGIP interaction mode
-    -c           tell ML system to compress output image
     -e MLTEXT    pass MLTEXT to the ML session
     -f           pass 'Session.finish();' to the ML session
     -m MODE      add print mode for output
@@ -319,12 +318,6 @@
   read-only after terminating.  Thus subsequent invocations cause the
   logic image to be read-only automatically.
 
-  \medskip The @{verbatim "-c"} option tells the underlying ML system
-  to compress the output heap (fully transparently).  On Poly/ML for
-  example, the image is garbage collected and all stored values are
-  maximally shared, resulting in up to @{text "50%"} less disk space
-  consumption.
-
   \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be
   passed to the Isabelle session from the command line. Multiple
   @{verbatim "-e"}'s are evaluated in the given order. Strange things
diff -r 39fe8093b1df -r 1f5740424c69 doc-src/System/Thy/Presentation.thy
--- a/doc-src/System/Thy/Presentation.thy	Sun May 31 15:29:43 2009 +0200
+++ b/doc-src/System/Thy/Presentation.thy	Sun May 31 15:49:35 2009 +0200
@@ -446,7 +446,6 @@
     -T LEVEL     multithreading: trace level (default 0)
     -V VERSION   declare alternative document VERSION
     -b           build mode (output heap image, using current dir)
-    -c BOOL      tell ML system to compress output image (default true)
     -d FORMAT    build document as FORMAT (default false)
     -f NAME      use ML file NAME (default ROOT.ML)
     -g BOOL      generate session graph image for document (default false)
diff -r 39fe8093b1df -r 1f5740424c69 doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Sun May 31 15:29:43 2009 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Sun May 31 15:49:35 2009 +0200
@@ -280,7 +280,6 @@
     -S           secure mode -- disallow critical operations
     -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream
     -X           startup PGIP interaction mode
-    -c           tell ML system to compress output image
     -e MLTEXT    pass MLTEXT to the ML session
     -f           pass 'Session.finish();' to the ML session
     -m MODE      add print mode for output
@@ -330,12 +329,6 @@
   read-only after terminating.  Thus subsequent invocations cause the
   logic image to be read-only automatically.
 
-  \medskip The \verb|-c| option tells the underlying ML system
-  to compress the output heap (fully transparently).  On Poly/ML for
-  example, the image is garbage collected and all stored values are
-  maximally shared, resulting in up to \isa{{\isachardoublequote}{\isadigit{5}}{\isadigit{0}}{\isacharpercent}{\isachardoublequote}} less disk space
-  consumption.
-
   \medskip Using the \verb|-e| option, arbitrary ML code may be
   passed to the Isabelle session from the command line. Multiple
   \verb|-e|'s are evaluated in the given order. Strange things
diff -r 39fe8093b1df -r 1f5740424c69 doc-src/System/Thy/document/Presentation.tex
--- a/doc-src/System/Thy/document/Presentation.tex	Sun May 31 15:29:43 2009 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex	Sun May 31 15:49:35 2009 +0200
@@ -472,7 +472,6 @@
     -T LEVEL     multithreading: trace level (default 0)
     -V VERSION   declare alternative document VERSION
     -b           build mode (output heap image, using current dir)
-    -c BOOL      tell ML system to compress output image (default true)
     -d FORMAT    build document as FORMAT (default false)
     -f NAME      use ML file NAME (default ROOT.ML)
     -g BOOL      generate session graph image for document (default false)
diff -r 39fe8093b1df -r 1f5740424c69 lib/Tools/usedir
--- a/lib/Tools/usedir	Sun May 31 15:29:43 2009 +0200
+++ b/lib/Tools/usedir	Sun May 31 15:49:35 2009 +0200
@@ -23,7 +23,6 @@
   echo "    -T LEVEL     multithreading: trace level (default 0)"
   echo "    -V VERSION   declare alternative document VERSION"
   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 "    -f NAME      use ML file NAME (default ROOT.ML)"
   echo "    -g BOOL      generate session graph image for document (default false)"
@@ -77,7 +76,6 @@
 TRACETHREADS="0"
 DOCUMENT_VERSIONS=""
 BUILD=""
-COMPRESS=true
 DOCUMENT=false
 ROOT_FILE="ROOT.ML"
 DOCUMENT_GRAPH=false
@@ -91,7 +89,7 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "C:D:M:P:Q:T:V:bc:d:f:g:i:m:p:rs:v:" OPT
+  while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:v:" OPT
   do
     case "$OPT" in
       C)
@@ -129,10 +127,6 @@
       b)
         BUILD=true
         ;;
-      c)
-        check_bool "$OPTARG"
-        COMPRESS="$OPTARG"
-        ;;
       d)
         DOCUMENT="$OPTARG"
         ;;
@@ -234,12 +228,9 @@
   echo "Building $ITEM ..." >&2
   LOG="$LOGDIR/$ITEM"
 
-  OPT_C=""
-  [ "$COMPRESS" = true ] && OPT_C="-c"
-
   "$ISABELLE_PROCESS" \
     -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
-    $OPT_C -q -w $LOGIC $NAME > "$LOG"
+    -q -w $LOGIC $NAME > "$LOG"
   RC="$?"
 else
   ITEM=$(basename "$LOGIC")-"$SESSION"
diff -r 39fe8093b1df -r 1f5740424c69 lib/scripts/run-mosml
--- a/lib/scripts/run-mosml	Sun May 31 15:29:43 2009 +0200
+++ b/lib/scripts/run-mosml	Sun May 31 15:49:35 2009 +0200
@@ -4,7 +4,7 @@
 #
 # Moscow ML 2.00 startup script
 
-export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
 
 
 ## diagnostics
diff -r 39fe8093b1df -r 1f5740424c69 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Sun May 31 15:29:43 2009 +0200
+++ b/lib/scripts/run-polyml	Sun May 31 15:49:35 2009 +0200
@@ -4,7 +4,7 @@
 #
 # Poly/ML 5.1/5.2 startup script.
 
-export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
 
 
 ## diagnostics
@@ -54,11 +54,7 @@
 if [ -z "$OUTFILE" ]; then
   COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
 else
-  if [ -z "$COMPRESS" ]; then
-    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
-  else
-    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
-  fi
+  COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
 fi
 
diff -r 39fe8093b1df -r 1f5740424c69 lib/scripts/run-polyml-5.0
--- a/lib/scripts/run-polyml-5.0	Sun May 31 15:29:43 2009 +0200
+++ b/lib/scripts/run-polyml-5.0	Sun May 31 15:49:35 2009 +0200
@@ -4,7 +4,7 @@
 #
 # Poly/ML 5.0 startup script.
 
-export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
 
 
 ## diagnostics
@@ -54,11 +54,7 @@
 if [ -z "$OUTFILE" ]; then
   COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
 else
-  if [ -z "$COMPRESS" ]; then
-    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
-  else
-    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
-  fi
+  COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   rm -f "${OUTFILE}.o" || fail_out
 fi
diff -r 39fe8093b1df -r 1f5740424c69 lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Sun May 31 15:29:43 2009 +0200
+++ b/lib/scripts/run-smlnj	Sun May 31 15:49:35 2009 +0200
@@ -4,7 +4,7 @@
 #
 # SML/NJ startup script (for 110 or later).
 
-export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
 
 
 ## diagnostics
diff -r 39fe8093b1df -r 1f5740424c69 src/Pure/mk
--- a/src/Pure/mk	Sun May 31 15:29:43 2009 +0200
+++ b/src/Pure/mk	Sun May 31 15:49:35 2009 +0200
@@ -114,7 +114,7 @@
     -e "val ml_platform = \"$ML_PLATFORM\";" \
     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
     -e "ml_prompts \"ML> \" \"ML# \";" \
-    -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
+    -f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
   RC="$?"
 fi