src/Tools/jEdit/src/timing_dockable.scala
changeset 56372 fadb0fef09d7
parent 56208 06cc31dff138
child 56662 f373fb77e0a4
--- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -182,7 +182,7 @@
     val iterator =
       restriction match {
         case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
-        case None => snapshot.version.nodes.entries
+        case None => snapshot.version.nodes.iterator
       }
     val nodes_timing1 =
       (nodes_timing /: iterator)({ case (timing1, (name, node)) =>