equal
deleted
inserted
replaced
204 |
204 |
205 fun completion context space (xname, pos) = |
205 fun completion context space (xname, pos) = |
206 if Context_Position.is_visible_generic context andalso Position.is_reported pos |
206 if Context_Position.is_visible_generic context andalso Position.is_reported pos |
207 then |
207 then |
208 let |
208 let |
|
209 val x = Name.clean xname; |
209 val Name_Space {kind = k, internals, ...} = space; |
210 val Name_Space {kind = k, internals, ...} = space; |
210 val ext = extern_shortest (Context.proof_of context) space; |
211 val ext = extern_shortest (Context.proof_of context) space; |
211 val names = |
212 val names = |
212 Symtab.fold |
213 Symtab.fold |
213 (fn (a, (b :: _, _)) => String.isPrefix xname a ? cons (ext b, Long_Name.implode [k, b]) |
214 (fn (a, (b :: _, _)) => String.isPrefix x a ? cons (ext b, Long_Name.implode [k, b]) |
214 | _ => I) internals [] |
215 | _ => I) internals [] |
215 |> sort_distinct (string_ord o pairself #1); |
216 |> sort_distinct (string_ord o pairself #1); |
216 in Completion.names pos names end |
217 in Completion.names pos names end |
217 else Completion.none; |
218 else Completion.none; |
218 |
219 |