special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;
authorwenzelm
Thu Mar 06 21:32:09 2014 +0100 (2014-03-06)
changeset 55962fbd0e768bc8f
parent 55961 c2d4a3608441
child 55963 a8ebafaa56d4
special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;
src/Pure/General/name_space.ML
src/Pure/Syntax/lexicon.ML
     1.1 --- a/src/Pure/General/name_space.ML	Thu Mar 06 20:26:43 2014 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Mar 06 21:32:09 2014 +0100
     1.3 @@ -322,6 +322,8 @@
     1.4  fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
     1.5    | transform_binding _ = I;
     1.6  
     1.7 +val bad_specs = ["", "??", "__"];
     1.8 +
     1.9  fun name_spec (naming as Naming {path, ...}) raw_binding =
    1.10    let
    1.11      val binding = transform_binding naming raw_binding;
    1.12 @@ -332,7 +334,7 @@
    1.13      val spec2 = if name = "" then [] else [(name, true)];
    1.14      val spec = spec1 @ spec2;
    1.15      val _ =
    1.16 -      exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
    1.17 +      exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
    1.18        andalso err_bad binding;
    1.19    in (concealed, if null spec2 then [] else spec) end;
    1.20  
     2.1 --- a/src/Pure/Syntax/lexicon.ML	Thu Mar 06 20:26:43 2014 +0100
     2.2 +++ b/src/Pure/Syntax/lexicon.ML	Thu Mar 06 21:32:09 2014 +0100
     2.3 @@ -261,8 +261,8 @@
     2.4  fun tokenize lex xids syms =
     2.5    let
     2.6      val scan_xid =
     2.7 -      if xids then $$$ "_" @@@ scan_id || scan_id
     2.8 -      else scan_id;
     2.9 +      (if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) ||
    2.10 +      $$$ "_" @@@ $$$ "_";
    2.11  
    2.12      val scan_num = scan_hex || scan_bin || scan_int;
    2.13