more restrictive completion: intern/extern stability;
authorwenzelm
Mon Mar 10 09:54:01 2014 +0100 (2014-03-10)
changeset 560228c9ab5d91d5a
parent 56015 57e2cfba9c6e
child 56023 f252a315c26e
more restrictive completion: intern/extern stability;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Sun Mar 09 22:45:09 2014 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Mon Mar 10 09:54:01 2014 +0100
     1.3 @@ -214,7 +214,10 @@
     1.4          Symtab.fold
     1.5            (fn (a, (name :: _, _)) =>
     1.6                if String.isPrefix x a andalso not (is_concealed space name)
     1.7 -              then cons (ext name, (kind, name)) else I
     1.8 +              then
     1.9 +                let val a' = ext name
    1.10 +                in if a = a' then cons (a', (kind, name)) else I end
    1.11 +              else I
    1.12              | _ => I) internals []
    1.13          |> sort_distinct (string_ord o pairself #1);
    1.14      in Completion.names pos names end