removed "compress" option from isabelle-process and isabelle usedir -- this is always enabled;
--- 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)
--- 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"
--- 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
--- 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)
--- 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
--- 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)
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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