src/Pure/library.scala

--- a/src/Pure/library.scala	Wed Aug 31 17:22:49 2011 +0200
+++ b/src/Pure/library.scala	Wed Aug 31 17:36:10 2011 +0200
@@ -14,6 +14,7 @@
 import scala.swing.ComboBox
 import scala.swing.event.SelectionChanged
 import scala.collection.mutable
+import scala.util.Sorting
 
 
 object Library
@@ -61,6 +62,13 @@
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
+  def sort_strings(args: Seq[String]): List[String] =
+  {
+    val a = args.toArray
+    Sorting.quickSort(a)
+    a.toList
+  }
+
 
   /* iterate over chunks (cf. space_explode) */