# HG changeset patch
# User wenzelm
# Date 1439901805 -7200
# Node ID eb87fc42825c19f76535a7f57387725bd4d340b6
# Parent  ad3c5eb9e348da570a0bd2743eaba87e5ec007fe
proper platform path for intial PolyML.SaveState.loadState;
tuned signature;

diff -r ad3c5eb9e348 -r eb87fc42825c lib/scripts/run-polyml-5.5.3
--- a/lib/scripts/run-polyml-5.5.3	Tue Aug 18 14:28:29 2015 +0200
+++ b/lib/scripts/run-polyml-5.5.3	Tue Aug 18 14:43:25 2015 +0200
@@ -40,6 +40,17 @@
 
 ## prepare databases
 
+case "$ML_PLATFORM" in
+  *-windows)
+    PLATFORM_INFILE="$(jvmpath -m "$INFILE")"
+    PLATFORM_OUTFILE="$(jvmpath -m "$OUTFILE")"
+    ;;
+  *)
+    PLATFORM_INFILE="$INFILE"
+    PLATFORM_OUTFILE="$OUTFILE"
+    ;;
+esac
+
 if [ -z "$INFILE" ]; then
   INIT=""
   case "$ML_PLATFORM" in
@@ -52,14 +63,6 @@
   esac
 else
   check_file "$INFILE"
-  case "$ML_PLATFORM" in
-    *-windows)
-      PLATFORM_INFILE="$(jvmpath -m "$INFILE")"
-      ;;
-    *)
-      PLATFORM_INFILE="$INFILE"
-      ;;
-  esac
   INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
   EXIT=""
 fi
@@ -68,7 +71,7 @@
   MLEXIT=""
 else
   if [ -z "$INFILE" ]; then
-    MLEXIT="(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\"); OS.Process.exit OS.Process.success);"
+    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);"
   else
     MLEXIT="Session.save \"$OUTFILE\";"
   fi
diff -r ad3c5eb9e348 -r eb87fc42825c src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Tue Aug 18 14:28:29 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Aug 18 14:43:25 2015 +0200
@@ -38,12 +38,9 @@
 
 structure ML_System =
 struct
-
-open ML_System;
-
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-val save_state = PolyML.SaveState.saveState;
-
+  open ML_System;
+  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+  val save_state = PolyML.SaveState.saveState o ml_platform_path;
 end;
 
 
diff -r ad3c5eb9e348 -r eb87fc42825c src/Pure/ML-Systems/windows_polyml.ML
--- a/src/Pure/ML-Systems/windows_polyml.ML	Tue Aug 18 14:28:29 2015 +0200
+++ b/src/Pure/ML-Systems/windows_polyml.ML	Tue Aug 18 14:43:25 2015 +0200
@@ -74,14 +74,3 @@
   val openOut = openOut o ml_platform_path;
   val openAppend = openAppend o ml_platform_path;
 end;
-
-structure PolyML =
-struct
-  open PolyML
-  structure SaveState =
-  struct
-    open SaveState;
-    val loadState = loadState o ml_platform_path;
-    val saveState = saveState o ml_platform_path;
-  end;
-end;