removed -c option;
authorwenzelm
Fri Apr 25 15:08:52 1997 +0200 (1997-04-25)
changeset 3054c16029f41ad9
parent 3053 db72904b42fb
child 3055 5da4afa207ad
removed -c option;
bin/isabelle
lib/Tools/usedir
     1.1 --- a/bin/isabelle	Fri Apr 25 15:08:25 1997 +0200
     1.2 +++ b/bin/isabelle	Fri Apr 25 15:08:52 1997 +0200
     1.3 @@ -22,7 +22,6 @@
     1.4    echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
     1.5    echo
     1.6    echo "  Options are:"
     1.7 -  echo "    -c           force copying of heap file (for Poly/ML)"
     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 @@ -48,19 +47,14 @@
    1.12  
    1.13  # options
    1.14  
    1.15 -COPYDB=""
    1.16  MLTEXT=""
    1.17 -COPYDB=""
    1.18  MODES=""
    1.19  TERMINATE=""
    1.20  READONLY=""
    1.21  
    1.22 -while getopts "ce:m:qru" OPT
    1.23 +while getopts "e:m:qru" OPT
    1.24  do
    1.25    case "$OPT" in
    1.26 -    c)
    1.27 -      COPYDB=true
    1.28 -      ;;
    1.29      e)
    1.30        MLTEXT="$MLTEXT $OPTARG"
    1.31        ;;
    1.32 @@ -166,6 +160,6 @@
    1.33  
    1.34  [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
    1.35  
    1.36 -export INFILE OUTFILE COPYDB MLTEXT TERMINATE
    1.37 +export INFILE OUTFILE MLTEXT TERMINATE
    1.38  [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
    1.39  exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
     2.1 --- a/lib/Tools/usedir	Fri Apr 25 15:08:25 1997 +0200
     2.2 +++ b/lib/Tools/usedir	Fri Apr 25 15:08:52 1997 +0200
     2.3 @@ -16,7 +16,6 @@
     2.4    echo
     2.5    echo "  Options are:"
     2.6    echo "    -b           build mode (output heap image, use dir \".\")"
     2.7 -  echo "    -c           force copying of heap file (for Poly/ML)"
     2.8    echo "    -g BOOL      generate theory graph data (default false)"
     2.9    echo "    -h BOOL      generate theory HTML data (default false)"
    2.10    echo "    -s NAME      override session NAME"
    2.11 @@ -33,7 +32,6 @@
    2.12  # options
    2.13  
    2.14  BUILD=""
    2.15 -COPYDB=""
    2.16  GRAPH=false
    2.17  HTML=false
    2.18  SESSION=""
    2.19 @@ -47,9 +45,6 @@
    2.20        b)
    2.21          BUILD=true
    2.22          ;;
    2.23 -      c)
    2.24 -        COPYDB="-c"
    2.25 -        ;;
    2.26        g)
    2.27          GRAPH="$OPTARG"
    2.28          ;;
    2.29 @@ -90,7 +85,7 @@
    2.30      -e "make_html := $HTML;" \
    2.31      -e "set_session\"$SESSION\";" \
    2.32      -e "exit_use_dir\".\";" \
    2.33 -    -q $COPYDB $LOGIC $NAME
    2.34 +    -q $LOGIC $NAME
    2.35  else
    2.36    exec $ISABELLE \
    2.37      -e "make_html := $HTML;" \