more structured order;
authorwenzelm
Mon Mar 10 10:13:47 2014 +0100 (2014-03-10)
changeset 560240921c1dc344c
parent 56023 f252a315c26e
child 56025 d74fed45fa8b
more structured order;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Mon Mar 10 10:04:26 2014 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Mon Mar 10 10:13:47 2014 +0100
     1.3 @@ -207,6 +207,10 @@
     1.4  fun completion context space (xname, pos) =
     1.5    if Position.is_reported pos andalso xname <> "" andalso xname <> "_" then
     1.6      let
     1.7 +      fun result_ord ((s, _), (s', _)) =
     1.8 +        (case int_ord (pairself Long_Name.qualification (s, s')) of
     1.9 +          EQUAL => string_ord (s, s')
    1.10 +        | ord => ord);
    1.11        val x = Name.clean xname;
    1.12        val Name_Space {kind, internals, ...} = space;
    1.13        val ext = extern_shortest (Context.proof_of context) space;
    1.14 @@ -219,7 +223,7 @@
    1.15                  in if a = a' then cons (a', (kind, name)) else I end
    1.16                else I
    1.17              | _ => I) internals []
    1.18 -        |> sort_distinct (string_ord o pairself #1);
    1.19 +        |> sort_distinct result_ord;
    1.20      in Completion.names pos names end
    1.21    else Completion.none;
    1.22