# HG changeset patch
# User wenzelm
# Date 1440098098 -7200
# Node ID 531a48ae14259ad1872763fb204332d61668c18c
# Parent  89effcb342dfda69fd45930f903cc5c571611ecb
clarified modules;

diff -r 89effcb342df -r 531a48ae1425 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Aug 20 21:08:47 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Aug 20 21:14:58 2015 +0200
@@ -34,7 +34,7 @@
 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 ();
+if ML_System.platform_is_windows then use "ML-Systems/windows_path.ML" else ();
 
 structure ML_System =
 struct
diff -r 89effcb342df -r 531a48ae1425 src/Pure/ML-Systems/windows_path.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/windows_path.ML	Thu Aug 20 21:14:58 2015 +0200
@@ -0,0 +1,35 @@
+(*  Title:      Pure/ML-Systems/windows_path.ML
+    Author:     Makarius
+
+Windows file-system paths.
+*)
+
+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;
diff -r 89effcb342df -r 531a48ae1425 src/Pure/ML-Systems/windows_polyml.ML
--- a/src/Pure/ML-Systems/windows_polyml.ML	Thu Aug 20 21:08:47 2015 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(*  Title:      Pure/ML-Systems/windows_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;
diff -r 89effcb342df -r 531a48ae1425 src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Aug 20 21:08:47 2015 +0200
+++ b/src/Pure/ROOT	Thu Aug 20 21:14:58 2015 +0200
@@ -34,7 +34,7 @@
     "ML-Systems/universal.ML"
     "ML-Systems/unsynchronized.ML"
     "ML-Systems/use_context.ML"
-    "ML-Systems/windows_polyml.ML"
+    "ML-Systems/windows_path.ML"
 
 session Pure =
   global_theories Pure
@@ -70,7 +70,7 @@
     "ML-Systems/universal.ML"
     "ML-Systems/unsynchronized.ML"
     "ML-Systems/use_context.ML"
-    "ML-Systems/windows_polyml.ML"
+    "ML-Systems/windows_path.ML"
 
     "Concurrent/bash.ML"
     "Concurrent/bash_sequential.ML"