no completion of concealed names;
authorwenzelm
Fri Mar 07 11:48:11 2014 +0100 (2014-03-07)
changeset 559759962ca0875c9
parent 55974 c835a9379026
child 55976 43815ee659bc
no completion of concealed names;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Fri Mar 07 11:46:26 2014 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Fri Mar 07 11:48:11 2014 +0100
     1.3 @@ -208,11 +208,13 @@
     1.4    if Position.is_reported pos then
     1.5      let
     1.6        val x = Name.clean xname;
     1.7 -      val Name_Space {kind = k, internals, ...} = space;
     1.8 +      val Name_Space {kind, internals, ...} = space;
     1.9        val ext = extern_shortest (Context.proof_of context) space;
    1.10        val names =
    1.11          Symtab.fold
    1.12 -          (fn (a, (b :: _, _)) => String.isPrefix x a ? cons (ext b, Long_Name.implode [k, b])
    1.13 +          (fn (a, (name :: _, _)) =>
    1.14 +              if String.isPrefix x a andalso not (is_concealed space name)
    1.15 +              then cons (ext name, Long_Name.implode [kind, name]) else I
    1.16              | _ => I) internals []
    1.17          |> sort_distinct (string_ord o pairself #1);
    1.18      in Completion.names pos names end