equal
deleted
inserted
replaced
212 val ext = extern_shortest (Context.proof_of context) space; |
212 val ext = extern_shortest (Context.proof_of context) space; |
213 val names = |
213 val names = |
214 Symtab.fold |
214 Symtab.fold |
215 (fn (a, (name :: _, _)) => |
215 (fn (a, (name :: _, _)) => |
216 if String.isPrefix x a andalso not (is_concealed space name) |
216 if String.isPrefix x a andalso not (is_concealed space name) |
217 then cons (ext name, Long_Name.implode [kind, name]) else I |
217 then cons (ext name, (kind, name)) else I |
218 | _ => I) internals [] |
218 | _ => I) internals [] |
219 |> sort_distinct (string_ord o pairself #1); |
219 |> sort_distinct (string_ord o pairself #1); |
220 in Completion.names pos names end |
220 in Completion.names pos names end |
221 else Completion.none; |
221 else Completion.none; |
222 |
222 |