ignore special names that are treated differently for various sub-languages (main wild-card is identifier "__");
--- 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;