|
1 (* Title: Pure/General/binding.ML |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 |
|
4 Structured name bindings. |
|
5 *) |
|
6 |
|
7 signature BASIC_BINDING = |
|
8 sig |
|
9 val long_names: bool ref |
|
10 val short_names: bool ref |
|
11 val unique_names: bool ref |
|
12 end; |
|
13 |
|
14 signature BINDING = |
|
15 sig |
|
16 include BASIC_BINDING |
|
17 type T |
|
18 val binding_pos: string * Position.T -> T |
|
19 val binding: string -> T |
|
20 val no_binding: T |
|
21 val dest_binding: T -> (string * bool) list * string |
|
22 val is_nothing: T -> bool |
|
23 val pos_of: T -> Position.T |
|
24 |
|
25 val map_binding: ((string * bool) list * string -> (string * bool) list * string) |
|
26 -> T -> T |
|
27 val add_prefix: bool -> string -> T -> T |
|
28 val map_prefix: ((string * bool) list -> T -> T) -> T -> T |
|
29 val display: T -> string |
|
30 end |
|
31 |
|
32 structure Binding : BINDING = |
|
33 struct |
|
34 |
|
35 (** global flags **) |
|
36 |
|
37 val long_names = ref false; |
|
38 val short_names = ref false; |
|
39 val unique_names = ref true; |
|
40 |
|
41 |
|
42 (** binding representation **) |
|
43 |
|
44 datatype T = Binding of ((string * bool) list * string) * Position.T; |
|
45 (* (prefix components (with mandatory flag), base name, position) *) |
|
46 |
|
47 fun binding_pos (name, pos) = Binding (([], name), pos); |
|
48 fun binding name = binding_pos (name, Position.none); |
|
49 val no_binding = binding ""; |
|
50 |
|
51 fun pos_of (Binding (_, pos)) = pos; |
|
52 fun dest_binding (Binding (prefix_name, _)) = prefix_name; |
|
53 |
|
54 fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos); |
|
55 |
|
56 fun is_nothing (Binding ((_, name), _)) = name = ""; |
|
57 |
|
58 fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix" |
|
59 else (map_binding o apfst) (cons (prfx, sticky)) b; |
|
60 |
|
61 fun map_prefix f (Binding ((prefix, name), pos)) = |
|
62 f prefix (binding_pos (name, pos)); |
|
63 |
|
64 fun display (Binding ((prefix, name), _)) = |
|
65 let |
|
66 fun mk_prefix (prfx, true) = prfx |
|
67 | mk_prefix (prfx, false) = enclose "(" ")" prfx |
|
68 in if not (! long_names) orelse null prefix orelse name = "" then name |
|
69 else space_implode "." (map mk_prefix prefix) ^ ":" ^ name |
|
70 end; |
|
71 |
|
72 end; |
|
73 |
|
74 structure Basic_Binding : BASIC_BINDING = Binding; |
|
75 open Basic_Binding; |