author | wenzelm |
Tue, 18 Aug 2015 15:37:50 +0200 | |
changeset 60969 | 8fa408a560a5 |
parent 60967 | eb87fc42825c |
child 60970 | e08d868ceca9 |
permissions | -rw-r--r-- |
60969 | 1 |
(* Title: Pure/ML-Systems/windows_polyml.ML |
60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
diff
changeset
|
3 |
|
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
diff
changeset
|
4 |
Poly/ML support for native Windows (MinGW). |
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
diff
changeset
|
5 |
*) |
60963
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
6 |
|
60965 | 7 |
fun ml_platform_path path = |
8 |
if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then |
|
9 |
(case String.tokens (fn c => c = #"/") path of |
|
10 |
"cygdrive" :: drive :: arcs => |
|
11 |
let |
|
12 |
val vol = |
|
13 |
(case Char.fromString drive of |
|
14 |
NONE => drive ^ ":" |
|
15 |
| SOME d => String.str (Char.toUpper d) ^ ":"); |
|
16 |
in OS.Path.toString {vol = vol, arcs = arcs, isAbs = true} end |
|
17 |
| arcs => |
|
18 |
(case OS.Process.getEnv "CYGWIN_ROOT" of |
|
19 |
SOME root => |
|
20 |
OS.Path.concat (root, OS.Path.toString {vol = "", arcs = arcs, isAbs = false}) |
|
21 |
| NONE => raise Fail "Unknown environment variable CYGWIN_ROOT")) |
|
22 |
else String.translate (fn #"/" => "\\" | c => String.str c) path; |
|
23 |
||
24 |
fun ml_standard_path path = |
|
25 |
let |
|
26 |
val {vol, arcs, isAbs} = OS.Path.fromString path; |
|
27 |
val path' = String.translate (fn #"\\" => "/" | c => String.str c) path; |
|
28 |
in |
|
29 |
if isAbs then |
|
30 |
(case String.explode vol of |
|
31 |
[d, #":"] => |
|
32 |
String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs) |
|
33 |
| _ => path') |
|
34 |
else path' |
|
35 |
end; |
|
36 |
||
60963
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
37 |
structure OS = |
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
38 |
struct |
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
39 |
open OS; |
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
40 |
|
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
41 |
structure FileSys = |
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
42 |
struct |
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
43 |
open FileSys; |
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
44 |
|
60965 | 45 |
val openDir = openDir o ml_platform_path; |
60963
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
46 |
|
60965 | 47 |
val chDir = chDir o ml_platform_path; |
48 |
val getDir = ml_standard_path o getDir; |
|
49 |
val mkDir = mkDir o ml_platform_path; |
|
50 |
val rmDir = rmDir o ml_platform_path; |
|
51 |
val isDir = isDir o ml_platform_path; |
|
52 |
val isLink = isLink o ml_platform_path; |
|
53 |
val readLink = readLink o ml_platform_path; |
|
54 |
val fullPath = ml_standard_path o fullPath o ml_platform_path; |
|
55 |
val realPath = ml_standard_path o realPath o ml_platform_path; |
|
56 |
val modTime = modTime o ml_platform_path; |
|
57 |
val fileSize = fileSize o ml_platform_path; |
|
58 |
fun setTime (file, time) = FileSys.setTime (ml_platform_path file, time); |
|
59 |
val remove = remove o ml_platform_path; |
|
60 |
fun rename {old, new} = FileSys.rename {old = ml_platform_path old, new = ml_platform_path new}; |
|
60963
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
61 |
|
60965 | 62 |
fun access (file, modes) = FileSys.access (ml_platform_path file, modes); |
60963
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
63 |
|
60965 | 64 |
val tmpName = ml_standard_path o tmpName; |
60963
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
65 |
|
60965 | 66 |
val fileId = fileId o ml_platform_path; |
60963
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
67 |
end; |
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
68 |
end; |
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
69 |
|
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
70 |
structure TextIO = |
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
71 |
struct |
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
72 |
open TextIO; |
60965 | 73 |
val openIn = openIn o ml_platform_path; |
74 |
val openOut = openOut o ml_platform_path; |
|
75 |
val openAppend = openAppend o ml_platform_path; |
|
60963
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
76 |
end; |