allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;
1.1 --- a/src/Pure/General/name_space.ML Sun Mar 02 21:52:44 2014 +0100
1.2 +++ b/src/Pure/General/name_space.ML Sun Mar 02 22:03:27 2014 +0100
1.3 @@ -206,11 +206,12 @@
1.4 if Context_Position.is_visible_generic context andalso Position.is_reported pos
1.5 then
1.6 let
1.7 + val x = Name.clean xname;
1.8 val Name_Space {kind = k, internals, ...} = space;
1.9 val ext = extern_shortest (Context.proof_of context) space;
1.10 val names =
1.11 Symtab.fold
1.12 - (fn (a, (b :: _, _)) => String.isPrefix xname a ? cons (ext b, Long_Name.implode [k, b])
1.13 + (fn (a, (b :: _, _)) => String.isPrefix x a ? cons (ext b, Long_Name.implode [k, b])
1.14 | _ => I) internals []
1.15 |> sort_distinct (string_ord o pairself #1);
1.16 in Completion.names pos names end