src/Pure/General/name_space.ML
changeset 55977 ec4830499634
parent 55975 9962ca0875c9
child 55989 55827fc7c0dd
equal deleted inserted replaced
55976:43815ee659bc 55977:ec4830499634
   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