# HG changeset patch # User wenzelm # Date 1439899647 -7200 # Node ID 49c797cb9f4694f63ff131cce9807f7b62254af6 # Parent fdb82e722f8ac8dea33106277fb47723b8010a36 tuned signature; diff -r fdb82e722f8a -r 49c797cb9f46 src/Pure/ML-Systems/polyml.ML --- 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 = diff -r fdb82e722f8a -r 49c797cb9f46 src/Pure/ML-Systems/smlnj.ML --- 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"; diff -r fdb82e722f8a -r 49c797cb9f46 src/Pure/ML-Systems/windows_polyml.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;