--- a/bin/isabelle Fri Apr 25 15:08:25 1997 +0200
+++ b/bin/isabelle Fri Apr 25 15:08:52 1997 +0200
@@ -22,7 +22,6 @@
echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
echo
echo " Options are:"
- echo " -c force copying of heap file (for Poly/ML)"
echo " -e MLTEXT pass MLTEXT to the ML session"
echo " -m MODE add print mode for output"
echo " -q non-interactive session"
@@ -48,19 +47,14 @@
# options
-COPYDB=""
MLTEXT=""
-COPYDB=""
MODES=""
TERMINATE=""
READONLY=""
-while getopts "ce:m:qru" OPT
+while getopts "e:m:qru" OPT
do
case "$OPT" in
- c)
- COPYDB=true
- ;;
e)
MLTEXT="$MLTEXT $OPTARG"
;;
@@ -166,6 +160,6 @@
[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
-export INFILE OUTFILE COPYDB MLTEXT TERMINATE
+export INFILE OUTFILE MLTEXT TERMINATE
[ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
--- a/lib/Tools/usedir Fri Apr 25 15:08:25 1997 +0200
+++ b/lib/Tools/usedir Fri Apr 25 15:08:52 1997 +0200
@@ -16,7 +16,6 @@
echo
echo " Options are:"
echo " -b build mode (output heap image, use dir \".\")"
- echo " -c force copying of heap file (for Poly/ML)"
echo " -g BOOL generate theory graph data (default false)"
echo " -h BOOL generate theory HTML data (default false)"
echo " -s NAME override session NAME"
@@ -33,7 +32,6 @@
# options
BUILD=""
-COPYDB=""
GRAPH=false
HTML=false
SESSION=""
@@ -47,9 +45,6 @@
b)
BUILD=true
;;
- c)
- COPYDB="-c"
- ;;
g)
GRAPH="$OPTARG"
;;
@@ -90,7 +85,7 @@
-e "make_html := $HTML;" \
-e "set_session\"$SESSION\";" \
-e "exit_use_dir\".\";" \
- -q $COPYDB $LOGIC $NAME
+ -q $LOGIC $NAME
else
exec $ISABELLE \
-e "make_html := $HTML;" \