src/Pure/General/name_space.ML
changeset 56022 8c9ab5d91d5a
parent 55989 55827fc7c0dd
child 56024 0921c1dc344c
equal deleted inserted replaced
56015:57e2cfba9c6e 56022:8c9ab5d91d5a
   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, (kind, name)) else I
   217               then
       
   218                 let val a' = ext name
       
   219                 in if a = a' then cons (a', (kind, name)) else I end
       
   220               else I
   218             | _ => I) internals []
   221             | _ => I) internals []
   219         |> sort_distinct (string_ord o pairself #1);
   222         |> sort_distinct (string_ord o pairself #1);
   220     in Completion.names pos names end
   223     in Completion.names pos names end
   221   else Completion.none;
   224   else Completion.none;
   222 
   225