--- 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;
--- 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 =
--- 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";
--- 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;
--- 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;
--- 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;
--- 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;
--- 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"
--- 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 *)