Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
prefer high-level ML_System.share_common_data, ML_System.save_state -- except for bootstrap images (RAW, Pure);
authorwenzelm
Mon, 16 Sep 2013 12:37:54 +0200
changeset 53657 64942a1f7187
parent 53656 a3c5ff796d84
child 53658 9e8714b4661a
prefer high-level ML_System.share_common_data, ML_System.save_state -- except for bootstrap images (RAW, Pure);
lib/scripts/run-polyml file | annotate | diff | comparison | revisions
lib/scripts/run-polyml-5.5.1 file | annotate | diff | comparison | revisions
lib/scripts/run-smlnj file | annotate | diff | comparison | revisions 
--- a/lib/scripts/run-polyml	Mon Sep 16 11:46:24 2013 +0200
+++ b/lib/scripts/run-polyml	Mon Sep 16 12:37:54 2013 +0200
@@ -52,7 +52,11 @@
   COMMIT='fun commit () = false;'
   MLEXIT=""
 else
-  COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+  if [ -z "$INFILE" ]; then
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+  else
+    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+  fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   MLEXIT="commit();"
 fi
--- a/lib/scripts/run-polyml-5.5.1	Mon Sep 16 11:46:24 2013 +0200
+++ b/lib/scripts/run-polyml-5.5.1	Mon Sep 16 12:37:54 2013 +0200
@@ -53,7 +53,11 @@
   COMMIT='fun commit () = false;'
   MLEXIT=""
 else
-  COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+  if [ -z "$INFILE" ]; then
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+  else
+    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+  fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   MLEXIT="commit();"
 fi
--- a/lib/scripts/run-smlnj	Mon Sep 16 11:46:24 2013 +0200
+++ b/lib/scripts/run-smlnj	Mon Sep 16 12:37:54 2013 +0200
@@ -47,6 +47,8 @@
 check_mlhome_file "$SML"
 check_mlhome_file "$ARCH_N_OPSYS"
 
+eval $("$ARCH_N_OPSYS")
+
 
 
 ## prepare databases
@@ -63,7 +65,11 @@
   COMMIT='fun commit () = false;'
   MLEXIT=""
 else
-  COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");"
+  if [ -z "$INFILE" ]; then
+    COMMIT="fun commit () = if SMLofNJ.exportML \"$OUTFILE\" then () else OS.FileSys.rename {old = \"$OUTFILE.$ARCH-$OPSYS\", new = \"$OUTFILE\"};"
+  else
+    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+  fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   MLEXIT="commit();"
 fi
@@ -87,11 +93,7 @@
 ## fix heap file name and permissions
 
 if [ -n "$OUTFILE" ]; then
-  eval $("$ARCH_N_OPSYS")
-  [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ARCH-$OPSYS"
-  HEAP="$OUTFILE.$HEAP_SUFFIX"
-  check_heap_file "$HEAP" && mv "$HEAP" "$OUTFILE" && \
-    [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+  check_heap_file "$OUTFILE" && [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 fi
 
 exit "$RC"
isabelle