# HG changeset patch # User wenzelm # Date 1324039028 -3600 # Node ID 793bf5fa5fbf0471b54fefb95e1128240c5621a6 # Parent df887263a37978403d471f2d55de8d11d013b0f7 prefer sorting from Scala library; diff -r df887263a379 -r 793bf5fa5fbf src/Pure/General/scan.scala --- 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(", ", ", ")") diff -r df887263a379 -r 793bf5fa5fbf src/Pure/PIDE/document.scala --- 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)) } } diff -r df887263a379 -r 793bf5fa5fbf src/Pure/System/isabelle_system.scala --- 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 } diff -r df887263a379 -r 793bf5fa5fbf src/Pure/Thy/completion.scala --- 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 } diff -r df887263a379 -r 793bf5fa5fbf src/Pure/library.scala --- 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) */ diff -r df887263a379 -r 793bf5fa5fbf src/Tools/jEdit/src/isabelle_sidekick.scala --- 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( diff -r df887263a379 -r 793bf5fa5fbf src/Tools/jEdit/src/plugin.scala --- 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