more thorough error handling of load/save (see also c1be3072ea8f);
authorwenzelm
Wed, 13 Feb 2013 13:52:06 +0100
changeset 51099 2ef891f99d2c
parent 51098 22d5c010ef5c
child 51100 18daa3380ff7
more thorough error handling of load/save (see also c1be3072ea8f);
lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Wed Feb 13 13:31:38 2013 +0100
+++ b/lib/scripts/run-polyml	Wed Feb 13 13:52:06 2013 +0100
@@ -49,7 +49,7 @@
   EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
 else
   check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
   EXIT=""
 fi
 
@@ -57,7 +57,7 @@
   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);"
+  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);"
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   MLEXIT="commit();"
 fi