ignore special names that are treated differently for various sub-languages (main wild-card is identifier "__");
authorwenzelm
Fri Mar 07 22:19:52 2014 +0100 (2014-03-07)
changeset 5598955827fc7c0dd
parent 55988 ffe88d72afae
child 55990 41c6b99c5fb7
ignore special names that are treated differently for various sub-languages (main wild-card is identifier "__");
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Fri Mar 07 20:50:02 2014 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Fri Mar 07 22:19:52 2014 +0100
     1.3 @@ -205,7 +205,7 @@
     1.4  (* completion *)
     1.5  
     1.6  fun completion context space (xname, pos) =
     1.7 -  if Position.is_reported pos then
     1.8 +  if Position.is_reported pos andalso xname <> "" andalso xname <> "_" then
     1.9      let
    1.10        val x = Name.clean xname;
    1.11        val Name_Space {kind, internals, ...} = space;