1.1 --- a/lib/scripts/run-polyml-5.1	Sun Nov 04 17:12:14 2007 +0100
     1.2 +++ b/lib/scripts/run-polyml-5.1	Sun Nov 04 19:17:13 2007 +0100
     1.3 @@ -44,11 +44,11 @@
     1.4  ## prepare databases
     1.5  
     1.6  if [ -z "$INFILE" ]; then
     1.7 -  PRG="$POLY"
     1.8 +  INIT=""
     1.9    EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
    1.10  else
    1.11    check_file "$INFILE"
    1.12 -  PRG="$INFILE"
    1.13 +  INIT="PolyML.SaveState.loadState \"$INFILE\";"
    1.14    EXIT=""
    1.15  fi
    1.16  
    1.17 @@ -56,18 +56,17 @@
    1.18    COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
    1.19  else
    1.20    if [ -z "$COMPRESS" ]; then
    1.21 -    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
    1.22 +    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
    1.23    else
    1.24 -    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
    1.25 +    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
    1.26    fi
    1.27    [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    1.28 -  rm -f "${OUTFILE}.o" || fail_out
    1.29  fi
    1.30  
    1.31  
    1.32  ## run it!
    1.33  
    1.34 -MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $EXIT $COMMIT $MLTEXT"
    1.35 +MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
    1.36  MLEXIT="commit();"
    1.37  
    1.38  if [ -z "$TERMINATE" ]; then
    1.39 @@ -76,22 +75,10 @@
    1.40    FEEDER_OPTS="-q"
    1.41  fi
    1.42  
    1.43 -if [ "$PRG" = "$POLY" ]; then
    1.44 -  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    1.45 -    { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.46 -else
    1.47 -  "$ISABELLE_HOME/lib/scripts/feeder" -p -t "$MLEXIT" $FEEDER_OPTS | \
    1.48 -    { read FPID; "$PRG" -q $ML_OPTIONS "$MLTEXT"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.49 -fi
    1.50 +"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    1.51 +  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.52  RC="$?"
    1.53  
    1.54 -if [ -n "$OUTFILE" ]; then
    1.55 -  if [ -e "${OUTFILE}.o" ]; then
    1.56 -    cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml $POLY_LINK_OPTIONS || fail_out
    1.57 -    rm -f "${OUTFILE}.o"
    1.58 -    [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
    1.59 -  fi
    1.60 -  [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    1.61 -fi
    1.62 +[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    1.63  
    1.64  exit "$RC"