tuned signature;

--- a/src/Pure/ML-Systems/polyml.ML	Tue Aug 18 11:43:24 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Aug 18 14:07:27 2015 +0200
@@ -32,6 +32,8 @@
 else ();
 
 fun ml_platform_path (s: string) = s;
+fun ml_standard_path (s: string) = s;
+
 if ML_System.platform_is_windows then use "ML-Systems/windows_polyml.ML" else ();
 
 structure ML_System =

--- a/src/Pure/ML-Systems/smlnj.ML	Tue Aug 18 11:43:24 2015 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Tue Aug 18 14:07:27 2015 +0200
@@ -169,6 +169,7 @@
 (* ML system operations *)
 
 fun ml_platform_path (s: string) = s;
+fun ml_standard_path (s: string) = s;
 
 use "ML-Systems/ml_system.ML";
 

--- a/src/Pure/ML-Systems/windows_polyml.ML	Tue Aug 18 11:43:24 2015 +0200
+++ b/src/Pure/ML-Systems/windows_polyml.ML	Tue Aug 18 14:07:27 2015 +0200
@@ -1,78 +1,78 @@
-(*  Title:      Pure/ML-Systems/windows_polyml.ML
+(*  Title:      Pure/ML-Systems/ml_platform_path_polyml.ML
     Author:     Makarius
 
 Poly/ML support for native Windows (MinGW).
 *)
 
+fun ml_platform_path path =
+  if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then
+    (case String.tokens (fn c => c = #"/") path of
+      "cygdrive" :: drive :: arcs =>
+        let
+          val vol =
+            (case Char.fromString drive of
+              NONE => drive ^ ":"
+            | SOME d => String.str (Char.toUpper d) ^ ":");
+        in OS.Path.toString {vol = vol, arcs = arcs, isAbs = true} end
+    | arcs =>
+        (case OS.Process.getEnv "CYGWIN_ROOT" of
+          SOME root =>
+            OS.Path.concat (root, OS.Path.toString {vol = "", arcs = arcs, isAbs = false})
+        | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
+  else String.translate (fn #"/" => "\\" | c => String.str c) path;
+
+fun ml_standard_path path =
+  let
+    val {vol, arcs, isAbs} = OS.Path.fromString path;
+    val path' = String.translate (fn #"\\" => "/" | c => String.str c) path;
+  in
+    if isAbs then
+      (case String.explode vol of
+        [d, #":"] =>
+          String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs)
+      | _ => path')
+    else path'
+  end;
+
 structure OS =
 struct
-  fun windows path =
-    if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then
-      (case String.tokens (fn c => c = #"/") path of
-        "cygdrive" :: drive :: arcs =>
-          let
-            val vol =
-              (case Char.fromString drive of
-                NONE => drive ^ ":"
-              | SOME d => String.str (Char.toUpper d) ^ ":");
-          in OS.Path.toString {vol = vol, arcs = arcs, isAbs = true} end
-      | arcs =>
-          (case OS.Process.getEnv "CYGWIN_ROOT" of
-            SOME root =>
-              OS.Path.concat (root, OS.Path.toString {vol = "", arcs = arcs, isAbs = false})
-          | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
-    else String.translate (fn #"/" => "\\" | c => String.str c) path;
-
-  fun cygwin path =
-    let
-      val {vol, arcs, isAbs} = OS.Path.fromString path;
-      val path' = String.translate (fn #"\\" => "/" | c => String.str c) path;
-    in
-      if isAbs then
-        (case String.explode vol of
-          [d, #":"] =>
-            String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs)
-        | _ => path')
-      else path'
-    end;
-
   open OS;
 
   structure FileSys =
   struct
     open FileSys;
 
-    val openDir = openDir o windows;
+    val openDir = openDir o ml_platform_path;
 
-    val chDir = chDir o windows;
-    val getDir = cygwin o getDir;
-    val mkDir = mkDir o windows;
-    val rmDir = rmDir o windows;
-    val isDir = isDir o windows;
-    val isLink = isLink o windows;
-    val readLink = readLink o windows;
-    val fullPath = cygwin o fullPath o windows;
-    val realPath = cygwin o realPath o windows;
-    val modTime = modTime o windows;
-    val fileSize = fileSize o windows;
-    fun setTime (file, time) = FileSys.setTime (windows file, time);
-    val remove = remove o windows;
-    fun rename {old, new} = FileSys.rename {old = windows old, new = windows new};
+    val chDir = chDir o ml_platform_path;
+    val getDir = ml_standard_path o getDir;
+    val mkDir = mkDir o ml_platform_path;
+    val rmDir = rmDir o ml_platform_path;
+    val isDir = isDir o ml_platform_path;
+    val isLink = isLink o ml_platform_path;
+    val readLink = readLink o ml_platform_path;
+    val fullPath = ml_standard_path o fullPath o ml_platform_path;
+    val realPath = ml_standard_path o realPath o ml_platform_path;
+    val modTime = modTime o ml_platform_path;
+    val fileSize = fileSize o ml_platform_path;
+    fun setTime (file, time) = FileSys.setTime (ml_platform_path file, time);
+    val remove = remove o ml_platform_path;
+    fun rename {old, new} = FileSys.rename {old = ml_platform_path old, new = ml_platform_path new};
 
-    fun access (file, modes) = FileSys.access (windows file, modes);
+    fun access (file, modes) = FileSys.access (ml_platform_path file, modes);
 
-    val tmpName = cygwin o tmpName;
+    val tmpName = ml_standard_path o tmpName;
 
-    val fileId = fileId o windows;
+    val fileId = fileId o ml_platform_path;
   end;
 end;
 
 structure TextIO =
 struct
   open TextIO;
-  val openIn = openIn o OS.windows;
-  val openOut = openOut o OS.windows;
-  val openAppend = openAppend o OS.windows;
+  val openIn = openIn o ml_platform_path;
+  val openOut = openOut o ml_platform_path;
+  val openAppend = openAppend o ml_platform_path;
 end;
 
 structure PolyML =
@@ -81,9 +81,7 @@
   structure SaveState =
   struct
     open SaveState;
-    val loadState = loadState o OS.windows;
-    val saveState = saveState o OS.windows;
+    val loadState = loadState o ml_platform_path;
+    val saveState = saveState o ml_platform_path;
   end;
 end;
-
-val ml_platform_path = OS.windows;