# HG changeset patch
# User wenzelm
# Date 1395057524 -3600
# Node ID 23ec13bb3db6791ee7069c731cd0baefdd2c711b
# Parent  62f10624339a9a7a255e7723280c53f1becbed7a
tuned;

diff -r 62f10624339a -r 23ec13bb3db6 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Mon Mar 17 12:24:00 2014 +0100
+++ b/src/Pure/General/completion.scala	Mon Mar 17 12:58:44 2014 +0100
@@ -89,17 +89,6 @@
           frequency(item2.name) compare frequency(item1.name)
       }
 
-    def name_ordering: Ordering[Item] =
-      new Ordering[Item] {
-        def compare(item1: Item, item2: Item): Int =
-        {
-          frequency(item2.name) compare frequency(item2.name) match {
-            case 0 => item1.name compare item2.name
-            case ord => ord
-          }
-        }
-      }
-
     def save()
     {
       Isabelle_System.mkdirs(COMPLETION_HISTORY.dir)
@@ -431,7 +420,9 @@
           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.name_ordering)))
+        else
+          Some(Completion.Result(range, original, unique,
+            items.sortBy(_.name).sorted(history.ordering)))
 
       case _ => None
     }