# HG changeset patch
# User wenzelm
# Date 1393794207 -3600
# Node ID a05413276a0db1acd328fa5d97448e6272f4e6c2
# Parent  fc04c24ad9eecb0948eca4f98ca34a1a722f7e60
allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;

diff -r fc04c24ad9ee -r a05413276a0d src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun Mar 02 21:52:44 2014 +0100
+++ b/src/Pure/General/name_space.ML	Sun Mar 02 22:03:27 2014 +0100
@@ -206,11 +206,12 @@
   if Context_Position.is_visible_generic context andalso Position.is_reported pos
   then
     let
+      val x = Name.clean xname;
       val Name_Space {kind = k, internals, ...} = space;
       val ext = extern_shortest (Context.proof_of context) space;
       val names =
         Symtab.fold
-          (fn (a, (b :: _, _)) => String.isPrefix xname a ? cons (ext b, Long_Name.implode [k, b])
+          (fn (a, (b :: _, _)) => String.isPrefix x a ? cons (ext b, Long_Name.implode [k, b])
             | _ => I) internals []
         |> sort_distinct (string_ord o pairself #1);
     in Completion.names pos names end