changeset 45900 | 793bf5fa5fbf |
parent 45474 | f793dd5d84b2 |
child 46152 | 793cecd4ffc0 |
--- a/src/Pure/PIDE/document.scala Fri Dec 16 12:03:33 2011 +0100 +++ b/src/Pure/PIDE/document.scala Fri Dec 16 13:37:08 2011 +0100 @@ -183,8 +183,7 @@ for (imp <- header.imports; name <- names.get(imp)) yield(name) case Exn.Exn(_) => Nil } - Library.topological_order(next, - Library.sort_wrt((name: Node.Name) => name.node, nodes.keys.toList)) + Library.topological_order(next, nodes.keys.toList.sortBy(_.node)) } }