# HG changeset patch # User wenzelm # Date 1314889121 -7200 # Node ID 101c117494cd9fe15bd6bf33f4316fbffb07e9aa # Parent 3e666dcdcd32ce3e94d04c67840322d407dd52d7 sort wrt. theory name; diff -r 3e666dcdcd32 -r 101c117494cd src/Tools/jEdit/src/session_dockable.scala --- a/src/Tools/jEdit/src/session_dockable.scala Thu Sep 01 16:58:03 2011 +0200 +++ b/src/Tools/jEdit/src/session_dockable.scala Thu Sep 01 16:58:41 2011 +0200 @@ -93,7 +93,8 @@ if (nodes_status != nodes_status1) { nodes_status = nodes_status1 val order = - Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList) + Library.sort_wrt((name: Document.Node.Name) => name.theory, + nodes_status.keySet.toList) status.listData = order.map(name => name.theory + " " + nodes_status(name)) } }