sort wrt. theory name;
authorwenzelm
Thu, 01 Sep 2011 16:58:41 +0200
changeset 45518101c117494cd
parent 45517 3e666dcdcd32
child 45519 446fe2abe252
sort wrt. theory name;
src/Tools/jEdit/src/session_dockable.scala
     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        }