sort wrt. theory name;
1.1 --- a/src/Tools/jEdit/src/session_dockable.scala Thu Sep 01 16:58:03 2011 +0200
1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala Thu Sep 01 16:58:41 2011 +0200
1.3 @@ -93,7 +93,8 @@
1.4 if (nodes_status != nodes_status1) {
1.5 nodes_status = nodes_status1
1.6 val order =
1.7 - Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
1.8 + Library.sort_wrt((name: Document.Node.Name) => name.theory,
1.9 + nodes_status.keySet.toList)
1.10 status.listData = order.map(name => name.theory + " " + nodes_status(name))
1.11 }
1.12 }