# HG changeset patch
# User wenzelm
# Date 1394442827 -3600
# Node ID 0921c1dc344c9ebb83bbdaa31a65d10c693b7edf
# Parent  f252a315c26e459bf9c5263e88b06a79380c0546
more structured order;

diff -r f252a315c26e -r 0921c1dc344c src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Mar 10 10:04:26 2014 +0100
+++ b/src/Pure/General/name_space.ML	Mon Mar 10 10:13:47 2014 +0100
@@ -207,6 +207,10 @@
 fun completion context space (xname, pos) =
   if Position.is_reported pos andalso xname <> "" andalso xname <> "_" then
     let
+      fun result_ord ((s, _), (s', _)) =
+        (case int_ord (pairself Long_Name.qualification (s, s')) of
+          EQUAL => string_ord (s, s')
+        | ord => ord);
       val x = Name.clean xname;
       val Name_Space {kind, internals, ...} = space;
       val ext = extern_shortest (Context.proof_of context) space;
@@ -219,7 +223,7 @@
                 in if a = a' then cons (a', (kind, name)) else I end
               else I
             | _ => I) internals []
-        |> sort_distinct (string_ord o pairself #1);
+        |> sort_distinct result_ord;
     in Completion.names pos names end
   else Completion.none;