author | wenzelm |
Fri, 20 Sep 2024 14:28:13 +0200 | |
changeset 80910 | 406a85a25189 |
parent 80803 | 7e39c785ca5d |
permissions | -rw-r--r-- |
6118 | 1 |
(* Title: Pure/General/path.ML |
5011 | 2 |
Author: Markus Wenzel, TU Muenchen |
3 |
||
43601 | 4 |
Algebra of file-system paths: basic POSIX notation, extended by named |
5 |
roots (e.g. //foo) and variables (e.g. $BAR). |
|
5011 | 6 |
*) |
7 |
||
8 |
signature PATH = |
|
9 |
sig |
|
6183 | 10 |
eqtype T |
6460 | 11 |
val is_current: T -> bool |
6183 | 12 |
val current: T |
13 |
val root: T |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
14 |
val named_root: string -> T |
6183 | 15 |
val parent: T |
69670 | 16 |
val make: string list -> T |
6183 | 17 |
val basic: string -> T |
18 |
val variable: string -> T |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69366
diff
changeset
|
19 |
val has_parent: T -> bool |
6183 | 20 |
val is_absolute: T -> bool |
21 |
val is_basic: T -> bool |
|
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56136
diff
changeset
|
22 |
val starts_basic: T -> bool |
6183 | 23 |
val append: T -> T -> T |
6270 | 24 |
val appends: T list -> T |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
25 |
val implode: T -> string |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
26 |
val explode: string -> T |
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
27 |
val explode_pos: string * Position.T -> T * Position.T |
53045 | 28 |
val split: string -> T list |
80803
7e39c785ca5d
clarified modules: enable pretty.ML to use XML/YXML more directly;
wenzelm
parents:
80802
diff
changeset
|
29 |
val print_markup: T -> Markup.T * string |
43593 | 30 |
val print: T -> string |
14912 | 31 |
val dir: T -> T |
6183 | 32 |
val base: T -> T |
33 |
val ext: string -> T -> T |
|
72479 | 34 |
val platform_exe: T -> T |
14912 | 35 |
val split_ext: T -> T * string |
70013 | 36 |
val exe: T -> T |
6183 | 37 |
val expand: T -> T |
69366 | 38 |
val file_name: T -> string |
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
39 |
eqtype binding |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
40 |
val binding: T * Position.T -> binding |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
41 |
val binding0: T -> binding |
70020 | 42 |
val map_binding: (T -> T) -> binding -> binding |
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
43 |
val dest_binding: binding -> T * Position.T |
70048 | 44 |
val path_of_binding: binding -> T |
45 |
val pos_of_binding: binding -> Position.T |
|
70055
36fb663145e5
type Path.binding may be empty: check later via proper_binding;
wenzelm
parents:
70048
diff
changeset
|
46 |
val proper_binding: binding -> unit |
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
47 |
val implode_binding: binding -> string |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
48 |
val explode_binding: string * Position.T -> binding |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
49 |
val explode_binding0: string -> binding |
5011 | 50 |
end; |
51 |
||
6187 | 52 |
structure Path: PATH = |
5011 | 53 |
struct |
54 |
||
6183 | 55 |
(* path elements *) |
56 |
||
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
57 |
datatype elem = |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
58 |
Root of string | |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
59 |
Basic of string | |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
60 |
Variable of string | |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
61 |
Parent; |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
62 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
63 |
local |
6183 | 64 |
|
69547 | 65 |
fun err_elem msg s = error (msg ^ " path element " ^ quote s); |
6183 | 66 |
|
69548
415dc92050a6
more strict check: avoid confusion of Path.basic with Path.current / Path.parent;
wenzelm
parents:
69547
diff
changeset
|
67 |
val illegal_elem = ["", "~", "~~", ".", ".."]; |
69550
57ff523d9008
reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
wenzelm
parents:
69549
diff
changeset
|
68 |
val illegal_char = ["/", "\\", "$", ":", "\"", "'", "<", ">", "|", "?", "*"]; |
69547 | 69 |
|
69627 | 70 |
fun check_elem s = |
69547 | 71 |
if member (op =) illegal_elem s then err_elem "Illegal" s |
52106 | 72 |
else |
69549 | 73 |
(s, ()) |-> fold_string (fn c => fn () => |
69550
57ff523d9008
reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
wenzelm
parents:
69549
diff
changeset
|
74 |
if ord c < 32 then |
57ff523d9008
reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
wenzelm
parents:
69549
diff
changeset
|
75 |
err_elem ("Illegal control character " ^ string_of_int (ord c) ^ " in") s |
57ff523d9008
reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
wenzelm
parents:
69549
diff
changeset
|
76 |
else if member (op =) illegal_char c then |
69547 | 77 |
err_elem ("Illegal character " ^ quote c ^ " in") s |
69627 | 78 |
else ()); |
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
79 |
|
69784
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69670
diff
changeset
|
80 |
in |
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69670
diff
changeset
|
81 |
|
69627 | 82 |
val root_elem = Root o tap check_elem; |
83 |
val basic_elem = Basic o tap check_elem; |
|
84 |
val variable_elem = Variable o tap check_elem; |
|
6183 | 85 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
86 |
end; |
6183 | 87 |
|
88 |
||
5011 | 89 |
(* type path *) |
90 |
||
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
91 |
datatype T = Path of elem list; (*reversed elements*) |
6183 | 92 |
|
93 |
fun rep (Path xs) = xs; |
|
5011 | 94 |
|
6460 | 95 |
fun is_current (Path []) = true |
96 |
| is_current _ = false; |
|
97 |
||
5011 | 98 |
val current = Path []; |
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
99 |
val root = Path [Root ""]; |
52106 | 100 |
fun named_root s = Path [root_elem s]; |
69670 | 101 |
val make = Path o rev o map basic_elem; |
52106 | 102 |
fun basic s = Path [basic_elem s]; |
103 |
fun variable s = Path [variable_elem s]; |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
104 |
val parent = Path [Parent]; |
5011 | 105 |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69366
diff
changeset
|
106 |
fun has_parent (Path xs) = exists (fn Parent => true | _ => false) xs; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69366
diff
changeset
|
107 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
108 |
fun is_absolute (Path xs) = |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
109 |
(case try List.last xs of |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
110 |
SOME (Root _) => true |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
111 |
| _ => false); |
5011 | 112 |
|
6183 | 113 |
fun is_basic (Path [Basic _]) = true |
114 |
| is_basic _ = false; |
|
5011 | 115 |
|
69784
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69670
diff
changeset
|
116 |
fun all_basic (Path elems) = |
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69670
diff
changeset
|
117 |
forall (fn Basic _ => true | _ => false) elems; |
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69670
diff
changeset
|
118 |
|
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56136
diff
changeset
|
119 |
fun starts_basic (Path xs) = |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56136
diff
changeset
|
120 |
(case try List.last xs of |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56136
diff
changeset
|
121 |
SOME (Basic _) => true |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56136
diff
changeset
|
122 |
| _ => false); |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56136
diff
changeset
|
123 |
|
5011 | 124 |
|
125 |
(* append and norm *) |
|
126 |
||
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
127 |
fun apply (y as Root _) _ = [y] |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
128 |
| apply Parent (xs as (Root _ :: _)) = xs |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
129 |
| apply Parent (Basic _ :: rest) = rest |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
130 |
| apply y xs = y :: xs; |
5011 | 131 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
132 |
fun append (Path xs) (Path ys) = Path (fold_rev apply ys xs); |
15570 | 133 |
fun appends paths = Library.foldl (uncurry append) (current, paths); |
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
134 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
135 |
fun norm elems = fold_rev apply elems []; |
5011 | 136 |
|
6183 | 137 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
138 |
(* implode *) |
5011 | 139 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
140 |
local |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
141 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
142 |
fun implode_elem (Root "") = "" |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
143 |
| implode_elem (Root s) = "//" ^ s |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
144 |
| implode_elem (Basic s) = s |
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
145 |
| implode_elem (Variable s) = "$" ^ s |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
146 |
| implode_elem Parent = ".."; |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
147 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
148 |
in |
5011 | 149 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
150 |
fun implode_path (Path []) = "." |
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
151 |
| implode_path (Path [Root ""]) = "/" |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
152 |
| implode_path (Path xs) = space_implode "/" (rev (map implode_elem xs)); |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
153 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
154 |
end; |
5011 | 155 |
|
156 |
||
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
157 |
(* explode *) |
6183 | 158 |
|
52106 | 159 |
fun explode_path str = |
160 |
let |
|
161 |
fun explode_elem s = |
|
162 |
(if s = ".." then Parent |
|
163 |
else if s = "~" then Variable "USER_HOME" |
|
164 |
else if s = "~~" then Variable "ISABELLE_HOME" |
|
165 |
else |
|
166 |
(case try (unprefix "$") s of |
|
167 |
SOME s' => variable_elem s' |
|
168 |
| NONE => basic_elem s)) |
|
169 |
handle ERROR msg => cat_error msg ("The error(s) above occurred in " ^ quote str); |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
170 |
|
52106 | 171 |
val (roots, raw_elems) = |
67522 | 172 |
(case chop_prefix (equal "") (space_explode "/" str) |>> length of |
52106 | 173 |
(0, es) => ([], es) |
174 |
| (1, es) => ([Root ""], es) |
|
175 |
| (_, []) => ([Root ""], []) |
|
176 |
| (_, e :: es) => ([root_elem e], es)); |
|
177 |
val elems = raw_elems |> filter_out (fn c => c = "" orelse c = ".") |> map explode_elem; |
|
6183 | 178 |
|
52106 | 179 |
in Path (norm (rev elems @ roots)) end; |
6183 | 180 |
|
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
181 |
fun explode_pos (s, pos) = |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
182 |
(explode_path s handle ERROR msg => error (msg ^ Position.here pos), pos); |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
183 |
|
53045 | 184 |
fun split str = |
185 |
space_explode ":" str |
|
186 |
|> map_filter (fn s => if s = "" then NONE else SOME (explode_path s)); |
|
187 |
||
5011 | 188 |
|
43593 | 189 |
(* print *) |
190 |
||
80803
7e39c785ca5d
clarified modules: enable pretty.ML to use XML/YXML more directly;
wenzelm
parents:
80802
diff
changeset
|
191 |
fun print_markup path = |
43593 | 192 |
let val s = implode_path path |
80803
7e39c785ca5d
clarified modules: enable pretty.ML to use XML/YXML more directly;
wenzelm
parents:
80802
diff
changeset
|
193 |
in (Markup.path s, quote s) end; |
43593 | 194 |
|
80803
7e39c785ca5d
clarified modules: enable pretty.ML to use XML/YXML more directly;
wenzelm
parents:
80802
diff
changeset
|
195 |
val print = print_markup #-> Markup.markup; |
62663 | 196 |
|
43593 | 197 |
|
6183 | 198 |
(* base element *) |
199 |
||
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
200 |
fun split_path f (Path (Basic s :: xs)) = f (Path xs, s) |
43599 | 201 |
| split_path _ path = error ("Cannot split path into dir/base: " ^ print path); |
6183 | 202 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
203 |
val dir = split_path #1; |
7929 | 204 |
val base = split_path (fn (_, s) => Path [Basic s]); |
6183 | 205 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
206 |
fun ext "" = I |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
207 |
| ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e))); |
6183 | 208 |
|
72479 | 209 |
val platform_exe = ML_System.platform_is_windows ? ext "exe"; |
210 |
||
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
211 |
val split_ext = split_path (fn (prfx, s) => apfst (append prfx) |
67522 | 212 |
(case chop_suffix (fn c => c <> ".") (raw_explode s) of |
14912 | 213 |
([], _) => (Path [Basic s], "") |
33957 | 214 |
| (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e))); |
6319 | 215 |
|
70013 | 216 |
val exe = ML_System.platform_is_windows ? ext "exe"; |
217 |
||
6183 | 218 |
|
17827 | 219 |
(* expand variables *) |
5011 | 220 |
|
48658 | 221 |
fun eval (Variable s) = |
222 |
let val path = explode_path (getenv_strict s) in |
|
223 |
if exists (fn Variable _ => true | _ => false) (rep path) then |
|
224 |
error ("Illegal path variable nesting: " ^ s ^ "=" ^ print path) |
|
225 |
else rep path |
|
226 |
end |
|
17827 | 227 |
| eval x = [x]; |
5011 | 228 |
|
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19305
diff
changeset
|
229 |
val expand = rep #> maps eval #> norm #> Path; |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
230 |
|
69366 | 231 |
val file_name = implode_path o base o expand; |
232 |
||
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
233 |
|
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
234 |
(* binding: strictly monotonic path with position *) |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
235 |
|
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
236 |
datatype binding = Binding of T * Position.T; |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
237 |
|
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
238 |
fun binding (path, pos) = |
70055
36fb663145e5
type Path.binding may be empty: check later via proper_binding;
wenzelm
parents:
70048
diff
changeset
|
239 |
if all_basic path then Binding (path, pos) |
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
240 |
else error ("Bad path binding: " ^ print path ^ Position.here pos); |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
241 |
|
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
242 |
fun binding0 path = binding (path, Position.none); |
70020 | 243 |
|
244 |
fun map_binding f (Binding (path, pos)) = binding (f path, pos); |
|
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
245 |
|
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
246 |
fun dest_binding (Binding args) = args; |
70048 | 247 |
val path_of_binding = dest_binding #> #1; |
248 |
val pos_of_binding = dest_binding #> #2; |
|
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
249 |
|
70055
36fb663145e5
type Path.binding may be empty: check later via proper_binding;
wenzelm
parents:
70048
diff
changeset
|
250 |
fun proper_binding binding = |
36fb663145e5
type Path.binding may be empty: check later via proper_binding;
wenzelm
parents:
70048
diff
changeset
|
251 |
if is_current (path_of_binding binding) |
36fb663145e5
type Path.binding may be empty: check later via proper_binding;
wenzelm
parents:
70048
diff
changeset
|
252 |
then error ("Empty path" ^ Position.here (pos_of_binding binding)) |
36fb663145e5
type Path.binding may be empty: check later via proper_binding;
wenzelm
parents:
70048
diff
changeset
|
253 |
else (); |
36fb663145e5
type Path.binding may be empty: check later via proper_binding;
wenzelm
parents:
70048
diff
changeset
|
254 |
|
70048 | 255 |
val implode_binding = path_of_binding #> implode_path; |
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
256 |
|
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
257 |
val explode_binding = binding o explode_pos; |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
258 |
fun explode_binding0 s = explode_binding (s, Position.none); |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
259 |
|
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
260 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
261 |
(*final declarations of this structure!*) |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
262 |
val implode = implode_path; |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
263 |
val explode = explode_path; |
5011 | 264 |
|
265 |
end; |
|
72511
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72479
diff
changeset
|
266 |
|
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72479
diff
changeset
|
267 |
ML_system_overload (uncurry Path.append) "+"; |