allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;
authorwenzelm
Sun, 02 Mar 2014 22:03:27 +0100
changeset 57187a05413276a0d
parent 57186 fc04c24ad9ee
child 57188 b56fda32bf24
allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;
src/Pure/General/name_space.ML
     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