# HG changeset patch
# User wenzelm
# Date 1194200233 -3600
# Node ID f9237f6f3a8dc129e06f66b1c3f8b76dd392764a
# Parent  76d7f3fd4fb3884bc177078d62a4f4b3916bcd3c
replaced cc/ld phase by PolyML.SaveState.saveState (potentially more efficient);

diff -r 76d7f3fd4fb3 -r f9237f6f3a8d lib/scripts/run-polyml-5.1
--- a/lib/scripts/run-polyml-5.1	Sun Nov 04 17:12:14 2007 +0100
+++ b/lib/scripts/run-polyml-5.1	Sun Nov 04 19:17:13 2007 +0100
@@ -44,11 +44,11 @@
 ## prepare databases
 
 if [ -z "$INFILE" ]; then
-  PRG="$POLY"
+  INIT=""
   EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
 else
   check_file "$INFILE"
-  PRG="$INFILE"
+  INIT="PolyML.SaveState.loadState \"$INFILE\";"
   EXIT=""
 fi
 
@@ -56,18 +56,17 @@
   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);"
+    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.export (\"$OUTFILE\", PolyML.rootFunction); true);"
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
   fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-  rm -f "${OUTFILE}.o" || fail_out
 fi
 
 
 ## run it!
 
-MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $EXIT $COMMIT $MLTEXT"
+MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
 MLEXIT="commit();"
 
 if [ -z "$TERMINATE" ]; then
@@ -76,22 +75,10 @@
   FEEDER_OPTS="-q"
 fi
 
-if [ "$PRG" = "$POLY" ]; then
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-    { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-else
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -t "$MLEXIT" $FEEDER_OPTS | \
-    { read FPID; "$PRG" -q $ML_OPTIONS "$MLTEXT"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-fi
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
 RC="$?"
 
-if [ -n "$OUTFILE" ]; then
-  if [ -e "${OUTFILE}.o" ]; then
-    cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml $POLY_LINK_OPTIONS || fail_out
-    rm -f "${OUTFILE}.o"
-    [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
-  fi
-  [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-fi
+[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 
 exit "$RC"