# HG changeset patch
# User wenzelm
# Date 1394137929 -3600
# Node ID fbd0e768bc8f09e802e6d0b091665e4eec98ad29
# Parent  c2d4a3608441c1969ab4f66ac7aa7319bddf597e
special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;

diff -r c2d4a3608441 -r fbd0e768bc8f src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Mar 06 20:26:43 2014 +0100
+++ b/src/Pure/General/name_space.ML	Thu Mar 06 21:32:09 2014 +0100
@@ -322,6 +322,8 @@
 fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
   | transform_binding _ = I;
 
+val bad_specs = ["", "??", "__"];
+
 fun name_spec (naming as Naming {path, ...}) raw_binding =
   let
     val binding = transform_binding naming raw_binding;
@@ -332,7 +334,7 @@
     val spec2 = if name = "" then [] else [(name, true)];
     val spec = spec1 @ spec2;
     val _ =
-      exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
+      exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
       andalso err_bad binding;
   in (concealed, if null spec2 then [] else spec) end;
 
diff -r c2d4a3608441 -r fbd0e768bc8f src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Mar 06 20:26:43 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Thu Mar 06 21:32:09 2014 +0100
@@ -261,8 +261,8 @@
 fun tokenize lex xids syms =
   let
     val scan_xid =
-      if xids then $$$ "_" @@@ scan_id || scan_id
-      else scan_id;
+      (if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) ||
+      $$$ "_" @@@ $$$ "_";
 
     val scan_num = scan_hex || scan_bin || scan_int;