clarified completion ordering: prefer local names;

--- a/src/Pure/General/completion.scala	Sat Mar 15 11:59:18 2014 +0100
+++ b/src/Pure/General/completion.scala	Sat Mar 15 12:51:14 2014 +0100
@@ -86,10 +86,16 @@
     def ordering: Ordering[Item] =
       new Ordering[Item] {
         def compare(item1: Item, item2: Item): Int =
+          frequency(item2.name) compare frequency(item1.name)
+      }
+
+    def name_ordering: Ordering[Item] =
+      new Ordering[Item] {
+        def compare(item1: Item, item2: Item): Int =
         {
-          frequency(item1.name) compare frequency(item2.name) match {
+          frequency(item2.name) compare frequency(item2.name) match {
             case 0 => item1.name compare item2.name
-            case ord => - ord
+            case ord => ord
           }
         }
       }
@@ -415,7 +421,7 @@
           yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
 
         if (items.isEmpty) None
-        else Some(Completion.Result(range, original, unique, items.sorted(history.ordering)))
+        else Some(Completion.Result(range, original, unique, items.sorted(history.name_ordering)))
 
       case _ => None
     }

--- a/src/Pure/General/long_name.ML	Sat Mar 15 11:59:18 2014 +0100
+++ b/src/Pure/General/long_name.ML	Sat Mar 15 12:51:14 2014 +0100
@@ -10,6 +10,8 @@
   val is_qualified: string -> bool
   val hidden: string -> string
   val is_hidden: string -> bool
+  val localN: string
+  val is_local: string -> bool
   val implode: string list -> string
   val explode: string -> string list
   val append: string -> string -> string
@@ -29,6 +31,9 @@
 fun hidden name = "??." ^ name;
 val is_hidden = String.isPrefix "??.";
 
+val localN = "local";
+val is_local = String.isPrefix "local.";
+
 val implode = space_implode separator;
 val explode = space_explode separator;
 

--- a/src/Pure/General/name_space.ML	Sat Mar 15 11:59:18 2014 +0100
+++ b/src/Pure/General/name_space.ML	Sat Mar 15 12:51:14 2014 +0100
@@ -224,9 +224,12 @@
 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')
+      fun result_ord ((xname1, (_, name1)), (xname2, (_, name2))) =
+        (case bool_ord (pairself Long_Name.is_local (name2, name1)) of
+          EQUAL =>
+            (case int_ord (pairself Long_Name.qualification (xname1, xname2)) of
+              EQUAL => string_ord (xname1, xname2)
+            | ord => ord)
         | ord => ord);
       val x = Name.clean xname;
       val Name_Space {kind, internals, ...} = space;
@@ -338,7 +341,7 @@
   path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
 
 val default_naming = make_naming (false, NONE, "", []);
-val local_naming = default_naming |> add_path "local";
+val local_naming = default_naming |> add_path Long_Name.localN;
 
 
 (* full name *)