equal
deleted
inserted
replaced
265 | ord => ord) |
265 | ord => ord) |
266 | ord => ord) |
266 | ord => ord) |
267 | ord => ord); |
267 | ord => ord); |
268 val Name_Space {kind, internals, ...} = space; |
268 val Name_Space {kind, internals, ...} = space; |
269 val ext = extern_shortest (Context.proof_of context) space; |
269 val ext = extern_shortest (Context.proof_of context) space; |
|
270 val full = Name.clean xname = ""; |
270 in |
271 in |
271 Change_Table.fold |
272 Change_Table.fold |
272 (fn (xname', (name :: _, _)) => |
273 (fn (xname', (name :: _, _)) => |
273 if completed xname' andalso not (is_concealed space name) then |
274 if completed xname' andalso not (is_concealed space name) then |
274 cons (xname' = ext name, (xname', (kind, name))) |
275 let val xname'' = ext name in |
275 else I |
276 if xname' <> xname'' andalso full then I |
|
277 else cons (xname' = xname'', (xname', (kind, name))) |
|
278 end |
|
279 else I |
276 | _ => I) internals [] |
280 | _ => I) internals [] |
277 |> sort_distinct result_ord |
281 |> sort_distinct result_ord |
278 |> map #2 |
282 |> map #2 |
279 end); |
283 end); |
280 |
284 |