# HG changeset patch
# User wenzelm
# Date 1394227192 -3600
# Node ID 55827fc7c0dd36d47fd6c5dee66017a6d886822d
# Parent  ffe88d72afae57ce74440071cf6d8f50a8e594c8
ignore special names that are treated differently for various sub-languages (main wild-card is identifier "__");

diff -r ffe88d72afae -r 55827fc7c0dd src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Mar 07 20:50:02 2014 +0100
+++ b/src/Pure/General/name_space.ML	Fri Mar 07 22:19:52 2014 +0100
@@ -205,7 +205,7 @@
 (* completion *)
 
 fun completion context space (xname, pos) =
-  if Position.is_reported pos then
+  if Position.is_reported pos andalso xname <> "" andalso xname <> "_" then
     let
       val x = Name.clean xname;
       val Name_Space {kind, internals, ...} = space;