60 val space_of_table: 'a table -> T |
60 val space_of_table: 'a table -> T |
61 val check_reports: Context.generic -> 'a table -> |
61 val check_reports: Context.generic -> 'a table -> |
62 xstring * Position.T list -> (string * Position.report list) * 'a |
62 xstring * Position.T list -> (string * Position.report list) * 'a |
63 val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a |
63 val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a |
64 val defined: 'a table -> string -> bool |
64 val defined: 'a table -> string -> bool |
|
65 val lookup: 'a table -> string -> 'a option |
65 val lookup_key: 'a table -> string -> (string * 'a) option |
66 val lookup_key: 'a table -> string -> (string * 'a) option |
66 val get: 'a table -> string -> 'a |
67 val get: 'a table -> string -> 'a |
67 val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table |
68 val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table |
68 val alias_table: naming -> binding -> string -> 'a table -> 'a table |
69 val alias_table: naming -> binding -> string -> 'a table -> 'a table |
69 val hide_table: bool -> string -> 'a table -> 'a table |
70 val hide_table: bool -> string -> 'a table -> 'a table |
160 | SOME (_, entry) => entry_markup false kind (name, entry)); |
161 | SOME (_, entry) => entry_markup false kind (name, entry)); |
161 |
162 |
162 fun is_concealed space name = #concealed (the_entry space name); |
163 fun is_concealed space name = #concealed (the_entry space name); |
163 |
164 |
164 |
165 |
165 (* name accesses *) |
166 (* intern *) |
166 |
167 |
167 fun lookup (Name_Space {internals, ...}) xname = |
168 fun intern' (Name_Space {internals, ...}) xname = |
168 (case Change_Table.lookup internals xname of |
169 (case Change_Table.lookup internals xname of |
169 NONE => (xname, true) |
170 NONE => (xname, true) |
170 | SOME ([], []) => (xname, true) |
171 | SOME ([], []) => (xname, true) |
171 | SOME ([name], _) => (name, true) |
172 | SOME ([name], _) => (name, true) |
172 | SOME (name :: _, _) => (name, false) |
173 | SOME (name :: _, _) => (name, false) |
173 | SOME ([], name' :: _) => (Long_Name.hidden name', true)); |
174 | SOME ([], name' :: _) => (Long_Name.hidden name', true)); |
174 |
175 |
|
176 val intern = #1 oo intern'; |
|
177 |
175 fun get_accesses (Name_Space {entries, ...}) name = |
178 fun get_accesses (Name_Space {entries, ...}) name = |
176 (case Change_Table.lookup entries name of |
179 (case Change_Table.lookup entries name of |
177 NONE => [name] |
180 NONE => [name] |
178 | SOME (externals, _) => externals); |
181 | SOME (externals, _) => externals); |
179 |
182 |
180 fun valid_accesses (Name_Space {internals, ...}) name = |
183 fun valid_accesses (Name_Space {internals, ...}) name = |
181 Change_Table.fold (fn (xname, (names, _)) => |
184 Change_Table.fold (fn (xname, (names, _)) => |
182 if not (null names) andalso hd names = name then cons xname else I) internals []; |
185 if not (null names) andalso hd names = name then cons xname else I) internals []; |
183 |
|
184 |
|
185 (* intern *) |
|
186 |
|
187 fun intern space xname = #1 (lookup space xname); |
|
188 |
186 |
189 |
187 |
190 (* extern *) |
188 (* extern *) |
191 |
189 |
192 val names_long_raw = Config.declare_option ("names_long", @{here}); |
190 val names_long_raw = Config.declare_option ("names_long", @{here}); |
203 val names_long = Config.get ctxt names_long; |
201 val names_long = Config.get ctxt names_long; |
204 val names_short = Config.get ctxt names_short; |
202 val names_short = Config.get ctxt names_short; |
205 val names_unique = Config.get ctxt names_unique; |
203 val names_unique = Config.get ctxt names_unique; |
206 |
204 |
207 fun valid require_unique xname = |
205 fun valid require_unique xname = |
208 let val (name', is_unique) = lookup space xname |
206 let val (name', is_unique) = intern' space xname |
209 in name = name' andalso (not require_unique orelse is_unique) end; |
207 in name = name' andalso (not require_unique orelse is_unique) end; |
210 |
208 |
211 fun ext [] = if valid false name then name else Long_Name.hidden name |
209 fun ext [] = if valid false name then name else Long_Name.hidden name |
212 | ext (nm :: nms) = if valid names_unique nm then nm else ext nms; |
210 | ext (nm :: nms) = if valid names_unique nm then nm else ext nms; |
213 in |
211 in |
494 val ((name, reports), x) = check_reports context table (xname, [pos]); |
492 val ((name, reports), x) = check_reports context table (xname, [pos]); |
495 val _ = Position.reports reports; |
493 val _ = Position.reports reports; |
496 in (name, x) end; |
494 in (name, x) end; |
497 |
495 |
498 fun defined (Table (_, tab)) name = Change_Table.defined tab name; |
496 fun defined (Table (_, tab)) name = Change_Table.defined tab name; |
|
497 fun lookup (Table (_, tab)) name = Change_Table.lookup tab name; |
499 fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name; |
498 fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name; |
500 |
499 |
501 fun get table name = |
500 fun get table name = |
502 (case lookup_key table name of |
501 (case lookup_key table name of |
503 SOME (_, x) => x |
502 SOME (_, x) => x |