--- a/bin/isabelle-process Sun May 31 15:07:03 2009 +0200
+++ b/bin/isabelle-process Sun May 31 15:27:19 2009 +0200
@@ -26,7 +26,6 @@
echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
echo
echo " Options are:"
- echo " -C tell ML system to copy output image"
echo " -I startup Isar interaction mode"
echo " -P startup Proof General interaction mode"
echo " -S secure mode -- disallow critical operations"
@@ -60,7 +59,6 @@
# options
-COPYDB=""
ISAR=false
PROOFGENERAL=""
SECURE=""
@@ -73,12 +71,9 @@
READONLY=""
NOWRITE=""
-while getopts "CIPSW:Xce:fm:qruw" OPT
+while getopts "IPSW:Xce:fm:qruw" OPT
do
case "$OPT" in
- C)
- COPYDB=true
- ;;
I)
ISAR=true
;;
@@ -235,8 +230,7 @@
NICE=""
fi
-export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \
- ISABELLE_PID ISABELLE_TMP
+export INFILE OUTFILE COMPRESS 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:07:03 2009 +0200
+++ b/doc-src/System/Thy/Basics.thy Sun May 31 15:27:19 2009 +0200
@@ -266,7 +266,6 @@
Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
Options are:
- -C tell ML system to copy output image
-I startup Isar interaction mode
-P startup Proof General interaction mode
-S secure mode -- disallow critical operations
@@ -326,10 +325,6 @@
maximally shared, resulting in up to @{text "50%"} less disk space
consumption.
- \medskip The @{verbatim "-C"} option tells the ML system to produce
- a completely self-contained output image, probably including a copy
- of the ML runtime system itself.
-
\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/document/Basics.tex Sun May 31 15:07:03 2009 +0200
+++ b/doc-src/System/Thy/document/Basics.tex Sun May 31 15:27:19 2009 +0200
@@ -275,7 +275,6 @@
Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
Options are:
- -C tell ML system to copy output image
-I startup Isar interaction mode
-P startup Proof General interaction mode
-S secure mode -- disallow critical operations
@@ -337,10 +336,6 @@
maximally shared, resulting in up to \isa{{\isachardoublequote}{\isadigit{5}}{\isadigit{0}}{\isacharpercent}{\isachardoublequote}} less disk space
consumption.
- \medskip The \verb|-C| option tells the ML system to produce
- a completely self-contained output image, probably including a copy
- of the ML runtime system itself.
-
\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/lib/scripts/run-mosml Sun May 31 15:07:03 2009 +0200
+++ b/lib/scripts/run-mosml Sun May 31 15:27:19 2009 +0200
@@ -4,7 +4,7 @@
#
# Moscow ML 2.00 startup script
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
## diagnostics
--- a/lib/scripts/run-polyml Sun May 31 15:07:03 2009 +0200
+++ b/lib/scripts/run-polyml Sun May 31 15:27:19 2009 +0200
@@ -4,7 +4,7 @@
#
# Poly/ML 5.1/5.2 startup script.
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
## diagnostics
--- a/lib/scripts/run-polyml-5.0 Sun May 31 15:07:03 2009 +0200
+++ b/lib/scripts/run-polyml-5.0 Sun May 31 15:27:19 2009 +0200
@@ -4,7 +4,7 @@
#
# Poly/ML 5.0 startup script.
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
## diagnostics
--- a/lib/scripts/run-smlnj Sun May 31 15:07:03 2009 +0200
+++ b/lib/scripts/run-smlnj Sun May 31 15:27:19 2009 +0200
@@ -4,7 +4,7 @@
#
# SML/NJ startup script (for 110 or later).
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
## diagnostics