more flexible sorting;
tuned display;

--- a/src/Pure/library.ML	Thu Sep 01 13:39:40 2011 +0200
+++ b/src/Pure/library.ML	Thu Sep 01 14:10:52 2011 +0200
@@ -959,7 +959,7 @@
 fun sort_distinct ord = quicksort true ord;
 
 val sort_strings = sort string_ord;
-fun sort_wrt sel xs = sort (string_ord o pairself sel) xs;
+fun sort_wrt key xs = sort (string_ord o pairself key) xs;
 
 
 (* items tagged by integer index *)

--- a/src/Pure/library.scala	Thu Sep 01 13:39:40 2011 +0200
+++ b/src/Pure/library.scala	Thu Sep 01 14:10:52 2011 +0200
@@ -14,6 +14,7 @@
 import scala.swing.ComboBox
 import scala.swing.event.SelectionChanged
 import scala.collection.mutable
+import scala.math.Ordering
 import scala.util.Sorting
 
 
@@ -62,13 +63,18 @@
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
-  def sort_strings(args: Seq[String]): List[String] =
+  def sort_wrt[A](key: A => String, args: Seq[A]): List[A] =
   {
-    val a = args.toArray
-    Sorting.quickSort(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/session_dockable.scala	Thu Sep 01 13:39:40 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Thu Sep 01 14:10:52 2011 +0200
@@ -73,7 +73,7 @@
 
   /* component state -- owned by Swing thread */
 
-  private var nodes_status: Map[String, String] = Map.empty
+  private var nodes_status: Map[Document.Node.Name, String] = Map.empty
 
   private def handle_changed(changed_nodes: Set[Document.Node.Name])
   {
@@ -88,12 +88,13 @@
             name <- changed_nodes
             node <- version.nodes.get(name)
             val status = Isar_Document.node_status(state, version, node)
-          } nodes_status1 += (name.node -> status.toString)
+          } nodes_status1 += (name -> status.toString)
 
           if (nodes_status != nodes_status1) {
             nodes_status = nodes_status1
-            val order = Library.sort_strings(nodes_status.keySet.toList)
-            status.listData = order.map(name => name + " " + nodes_status(name))
+            val order =
+              Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
+            status.listData = order.map(name => name.theory + " " + nodes_status(name))
           }
       }
     }