equal
deleted
inserted
replaced
4 File system operations. |
4 File system operations. |
5 *) |
5 *) |
6 |
6 |
7 signature FILE = |
7 signature FILE = |
8 sig |
8 sig |
|
9 val standard_path: Path.T -> string |
9 val platform_path: Path.T -> string |
10 val platform_path: Path.T -> string |
10 val shell_quote: string -> string |
11 val shell_quote: string -> string |
11 val shell_path: Path.T -> string |
12 val shell_path: Path.T -> string |
12 val cd: Path.T -> unit |
13 val cd: Path.T -> unit |
13 val pwd: unit -> Path.T |
14 val pwd: unit -> Path.T |
40 structure File: FILE = |
41 structure File: FILE = |
41 struct |
42 struct |
42 |
43 |
43 (* system path representations *) |
44 (* system path representations *) |
44 |
45 |
45 val platform_path = Path.implode o Path.expand; |
46 val standard_path = Path.implode o Path.expand; |
|
47 val platform_path = ml_platform_path o standard_path; |
46 |
48 |
47 val shell_quote = enclose "'" "'"; |
49 val shell_quote = enclose "'" "'"; |
48 val shell_path = shell_quote o platform_path; |
50 val shell_path = shell_quote o standard_path; |
49 |
51 |
50 |
52 |
51 (* current working directory *) |
53 (* current working directory *) |
52 |
54 |
53 val cd = cd o platform_path; |
55 val cd = cd o standard_path; |
54 val pwd = Path.explode o pwd; |
56 val pwd = Path.explode o pwd; |
55 |
57 |
56 |
58 |
57 (* full_path *) |
59 (* full_path *) |
58 |
60 |