prefer sorting from Scala library;

--- a/src/Pure/General/scan.scala	Fri Dec 16 12:03:33 2011 +0100
+++ b/src/Pure/General/scan.scala	Fri Dec 16 13:37:08 2011 +0100
@@ -79,7 +79,7 @@
 
     /* pseudo Set methods */
 
-    def iterator: Iterator[String] = content(main_tree, Nil).sortWith(_ <= _).iterator
+    def iterator: Iterator[String] = content(main_tree, Nil).sorted.iterator
 
     override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
 

--- a/src/Pure/PIDE/document.scala	Fri Dec 16 12:03:33 2011 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 16 13:37:08 2011 +0100
@@ -183,8 +183,7 @@
             for (imp <- header.imports; name <- names.get(imp)) yield(name)
           case Exn.Exn(_) => Nil
         }
-      Library.topological_order(next,
-        Library.sort_wrt((name: Node.Name) => name.node, nodes.keys.toList))
+      Library.topological_order(next, nodes.keys.toList.sortBy(_.node))
     }
   }
 

--- a/src/Pure/System/isabelle_system.scala	Fri Dec 16 12:03:33 2011 +0100
+++ b/src/Pure/System/isabelle_system.scala	Fri Dec 16 13:37:08 2011 +0100
@@ -297,7 +297,7 @@
         for (file <- files if file.isFile) logics += file.getName
       }
     }
-    logics.toList.sortWith(_ < _)
+    logics.toList.sorted
   }
 
 

--- a/src/Pure/Thy/completion.scala	Fri Dec 16 12:03:33 2011 +0100
+++ b/src/Pure/Thy/completion.scala	Fri Dec 16 13:37:08 2011 +0100
@@ -96,7 +96,7 @@
           case Some(word) =>
             words_lex.completions(word).map(words_map(_)) match {
               case Nil => None
-              case cs => Some(word, cs.sortWith(_ < _))
+              case cs => Some(word, cs.sorted)
             }
           case None => None
         }

--- a/src/Pure/library.scala	Fri Dec 16 12:03:33 2011 +0100
+++ b/src/Pure/library.scala	Fri Dec 16 13:37:08 2011 +0100
@@ -64,18 +64,6 @@
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
-  def sort_wrt[A](key: A => String, args: Seq[A]): List[A] =
-  {
-    val ordering: Ordering[A] =
-      new Ordering[A] { def compare(x: A, y: A): Int = key(x) compare key(y) }
-    val a = (new Array[Any](args.length)).asInstanceOf[Array[A]]
-    for ((x, i) <- args.iterator zipWithIndex) a(i) = x
-    Sorting.quickSort[A](a)(ordering)
-    a.toList
-  }
-
-  def sort_strings(args: Seq[String]): List[String] = sort_wrt((x: String) => x, args)
-
 
   /* iterate over chunks (cf. space_explode) */
 

--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Dec 16 12:03:33 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Dec 16 13:37:08 2011 +0100
@@ -96,7 +96,7 @@
             case Some((word, cs)) =>
               val ds =
                 (if (Isabelle_Encoding.is_active(buffer))
-                  cs.map(Symbol.decode(_)).sortWith(_ < _)
+                  cs.map(Symbol.decode(_)).sorted
                  else cs).filter(_ != word)
               if (ds.isEmpty) null
               else new SideKickCompletion(

--- a/src/Tools/jEdit/src/plugin.scala	Fri Dec 16 12:03:33 2011 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Dec 16 13:37:08 2011 +0100
@@ -379,7 +379,7 @@
         filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
 
       if (!files.isEmpty) {
-        val files_list = new ListView(Library.sort_strings(files))
+        val files_list = new ListView(files.sorted)
         for (i <- 0 until files.length)
           files_list.selection.indices += i