206 |
206 |
207 fun completion context space (xname, pos) = |
207 fun completion context space (xname, pos) = |
208 if Position.is_reported pos then |
208 if Position.is_reported pos then |
209 let |
209 let |
210 val x = Name.clean xname; |
210 val x = Name.clean xname; |
211 val Name_Space {kind = k, internals, ...} = space; |
211 val Name_Space {kind, internals, ...} = space; |
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, (b :: _, _)) => String.isPrefix x a ? cons (ext b, Long_Name.implode [k, b]) |
215 (fn (a, (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 |
216 | _ => I) internals [] |
218 | _ => I) internals [] |
217 |> sort_distinct (string_ord o pairself #1); |
219 |> sort_distinct (string_ord o pairself #1); |
218 in Completion.names pos names end |
220 in Completion.names pos names end |
219 else Completion.none; |
221 else Completion.none; |
220 |
222 |