more structured order;
authorwenzelm
Mon, 10 Mar 2014 10:13:47 +0100
changeset 56024 0921c1dc344c
parent 56023 f252a315c26e
child 56025 d74fed45fa8b
more structured order;
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;