# HG changeset patch
# User wenzelm
# Date 1456756757 -3600
# Node ID d97e13e5ea5b644351ac42ef43a56efad1d62693
# Parent  c1b88e647e2f42523965d83baae1e226d49eded6
clarified modules;

diff -r c1b88e647e2f -r d97e13e5ea5b src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Mon Feb 29 15:23:13 2016 +0100
+++ b/src/Pure/General/file.ML	Mon Feb 29 15:39:17 2016 +0100
@@ -45,7 +45,7 @@
 (* system path representations *)
 
 val standard_path = Path.implode o Path.expand;
-val platform_path = ml_platform_path o standard_path;
+val platform_path = ML_System.platform_path o standard_path;
 
 val shell_quote = enclose "'" "'";
 val shell_path = shell_quote o standard_path;
diff -r c1b88e647e2f -r d97e13e5ea5b src/Pure/ML/exn_properties.ML
--- a/src/Pure/ML/exn_properties.ML	Mon Feb 29 15:23:13 2016 +0100
+++ b/src/Pure/ML/exn_properties.ML	Mon Feb 29 15:39:17 2016 +0100
@@ -21,7 +21,7 @@
     [] => []
   | [XML.Text file] =>
       if file = "Standard Basis" then []
-      else [(Markup.fileN, ml_standard_path file)]
+      else [(Markup.fileN, ML_System.standard_path file)]
   | body => XML.Decode.properties body);
 
 fun position_of loc =
diff -r c1b88e647e2f -r d97e13e5ea5b src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Mon Feb 29 15:23:13 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Mon Feb 29 15:39:17 2016 +0100
@@ -31,11 +31,6 @@
 
 (* ML heap operations *)
 
-fun ml_platform_path (s: string) = s;
-fun ml_standard_path (s: string) = s;
-
-if ML_System.platform_is_windows then use "RAW/windows_path.ML" else ();
-
 if ML_System.name = "polyml-5.3.0"
 then use "RAW/ml_heap_polyml-5.3.0.ML"
 else use "RAW/ml_heap.ML";
diff -r c1b88e647e2f -r d97e13e5ea5b src/Pure/RAW/ml_heap.ML
--- a/src/Pure/RAW/ml_heap.ML	Mon Feb 29 15:23:13 2016 +0100
+++ b/src/Pure/RAW/ml_heap.ML	Mon Feb 29 15:39:17 2016 +0100
@@ -13,5 +13,5 @@
 structure ML_Heap: ML_HEAP =
 struct
   fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-  val save_state = PolyML.SaveState.saveState o ml_platform_path;
+  val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
 end;
diff -r c1b88e647e2f -r d97e13e5ea5b src/Pure/RAW/ml_heap_polyml-5.3.0.ML
--- a/src/Pure/RAW/ml_heap_polyml-5.3.0.ML	Mon Feb 29 15:23:13 2016 +0100
+++ b/src/Pure/RAW/ml_heap_polyml-5.3.0.ML	Mon Feb 29 15:39:17 2016 +0100
@@ -13,5 +13,5 @@
 structure ML_Heap: ML_HEAP =
 struct
   fun share_common_data () = ();
-  val save_state = PolyML.SaveState.saveState o ml_platform_path;
+  val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
 end;
diff -r c1b88e647e2f -r d97e13e5ea5b src/Pure/RAW/ml_system.ML
--- a/src/Pure/RAW/ml_system.ML	Mon Feb 29 15:23:13 2016 +0100
+++ b/src/Pure/RAW/ml_system.ML	Mon Feb 29 15:39:17 2016 +0100
@@ -9,6 +9,8 @@
   val name: string
   val platform: string
   val platform_is_windows: bool
+  val platform_path: string -> string
+  val standard_path: string -> string
 end;
 
 structure ML_System: ML_SYSTEM =
@@ -18,4 +20,39 @@
 val SOME platform = OS.Process.getEnv "ML_PLATFORM";
 val platform_is_windows = String.isSuffix "windows" platform;
 
+val platform_path =
+  if platform_is_windows then
+    fn 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 String.concatWith "\\" (vol :: arcs) end
+        | arcs =>
+            (case OS.Process.getEnv "CYGWIN_ROOT" of
+              SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
+            | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
+      else String.translate (fn #"/" => "\\" | c => String.str c) path
+  else fn path => path;
+
+val standard_path =
+  if platform_is_windows then
+    fn 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
+  else fn path => path;
+
 end;
diff -r c1b88e647e2f -r d97e13e5ea5b src/Pure/RAW/windows_path.ML
--- a/src/Pure/RAW/windows_path.ML	Mon Feb 29 15:23:13 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-(*  Title:      Pure/RAW/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 String.concatWith "\\" (vol :: arcs) end
-    | arcs =>
-        (case OS.Process.getEnv "CYGWIN_ROOT" of
-          SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
-        | 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 c1b88e647e2f -r d97e13e5ea5b src/Pure/ROOT
--- a/src/Pure/ROOT	Mon Feb 29 15:23:13 2016 +0100
+++ b/src/Pure/ROOT	Mon Feb 29 15:39:17 2016 +0100
@@ -31,7 +31,6 @@
     "RAW/single_assignment_polyml.ML"
     "RAW/unsynchronized.ML"
     "RAW/use_context.ML"
-    "RAW/windows_path.ML"
 
 session Pure =
   global_theories Pure
@@ -64,7 +63,6 @@
     "RAW/single_assignment_polyml.ML"
     "RAW/unsynchronized.ML"
     "RAW/use_context.ML"
-    "RAW/windows_path.ML"
 
     "Concurrent/bash.ML"
     "Concurrent/bash_windows.ML"
diff -r c1b88e647e2f -r d97e13e5ea5b src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Feb 29 15:23:13 2016 +0100
+++ b/src/Pure/library.ML	Mon Feb 29 15:39:17 2016 +0100
@@ -1031,8 +1031,8 @@
 
 (* current directory *)
 
-val cd = OS.FileSys.chDir o ml_platform_path;
-val pwd = ml_standard_path o OS.FileSys.getDir;
+val cd = OS.FileSys.chDir o ML_System.platform_path;
+val pwd = ML_System.standard_path o OS.FileSys.getDir;
 
 
 (* getenv *)