src/Pure/General/name_space.ML
changeset 55975 9962ca0875c9
parent 55962 fbd0e768bc8f
child 55977 ec4830499634
equal deleted inserted replaced
55974:c835a9379026 55975:9962ca0875c9
   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