equal
deleted
inserted
replaced
7 |
7 |
8 signature FILE = |
8 signature FILE = |
9 sig |
9 sig |
10 val sys_pack_fn: (Path.T -> string) ref |
10 val sys_pack_fn: (Path.T -> string) ref |
11 val sys_unpack_fn: (string -> Path.T) ref |
11 val sys_unpack_fn: (string -> Path.T) ref |
12 val use: Path.T -> unit |
|
13 val rm: Path.T -> unit |
12 val rm: Path.T -> unit |
14 val cd: Path.T -> unit |
13 val cd: Path.T -> unit |
15 val pwd: unit -> Path.T |
14 val pwd: unit -> Path.T |
16 val full_path: Path.T -> Path.T |
15 val full_path: Path.T -> Path.T |
17 val tmp_path: Path.T -> Path.T |
16 val tmp_path: Path.T -> Path.T |
21 val copy: Path.T -> Path.T -> unit |
20 val copy: Path.T -> Path.T -> unit |
22 eqtype info |
21 eqtype info |
23 val info: Path.T -> info option |
22 val info: Path.T -> info option |
24 val exists: Path.T -> bool |
23 val exists: Path.T -> bool |
25 val mkdir: Path.T -> unit |
24 val mkdir: Path.T -> unit |
|
25 val source: Path.T -> (string, string list) Source.source * Position.T |
|
26 val plain_use: Path.T -> unit |
|
27 val symbol_use: Path.T -> unit |
26 end; |
28 end; |
27 |
29 |
28 structure File: FILE = |
30 structure File: FILE = |
29 struct |
31 struct |
30 |
32 |
35 val sys_unpack_fn = ref Path.unpack; |
37 val sys_unpack_fn = ref Path.unpack; |
36 |
38 |
37 fun sysify path = ! sys_pack_fn (Path.expand path); |
39 fun sysify path = ! sys_pack_fn (Path.expand path); |
38 fun unsysify s = ! sys_unpack_fn s; |
40 fun unsysify s = ! sys_unpack_fn s; |
39 |
41 |
40 |
|
41 val use = use o sysify; |
|
42 val rm = OS.FileSys.remove o sysify; |
42 val rm = OS.FileSys.remove o sysify; |
43 |
43 |
44 |
44 |
45 (* current path *) |
45 (* current path *) |
46 |
46 |
91 (* mkdir *) |
91 (* mkdir *) |
92 |
92 |
93 fun mkdir path = (execute ("mkdir -p " ^ enclose "'" "'" (sysify path)); ()); |
93 fun mkdir path = (execute ("mkdir -p " ^ enclose "'" "'" (sysify path)); ()); |
94 |
94 |
95 |
95 |
|
96 (* source *) |
|
97 |
|
98 fun source raw_path = |
|
99 let val path = Path.expand raw_path |
|
100 in (Source.of_string (read path), Position.line_name 1 (quote (Path.pack path))) end; |
|
101 |
|
102 |
|
103 (* symbol_use *) |
|
104 |
|
105 val plain_use = use o sysify; |
|
106 |
|
107 (* version of 'use' with input filtering *) |
|
108 |
|
109 val symbol_use = |
|
110 if not needs_filtered_use then plain_use (*ML system (wrongly!) accepts non-ASCII*) |
|
111 else |
|
112 fn path => |
|
113 let |
|
114 val txt = read path; |
|
115 val txt_out = Symbol.input txt; |
|
116 in |
|
117 if txt = txt_out then plain_use path |
|
118 else |
|
119 let val tmp_path = tmp_path path in |
|
120 write tmp_path txt_out; |
|
121 plain_use tmp_path handle exn => (rm tmp_path; raise exn); |
|
122 rm tmp_path |
|
123 end |
|
124 end; |
|
125 |
96 end; |
126 end; |