src/Tools/jEdit/src/timing_dockable.scala
changeset 52888 671421cef590
parent 51549 37211c7c2894
child 52973 d5f7fa1498b7
--- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Aug 07 11:44:17 2013 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Aug 07 11:50:14 2013 +0200
@@ -167,7 +167,7 @@
         case None => Document.Node.Name.empty
         case Some(doc_view) => doc_view.model.name
       }
-    val timing = nodes_timing.get(name) getOrElse Protocol.empty_node_timing
+    val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing)
 
     val theories =
       (for ((node_name, node_timing) <- nodes_timing.toList if !node_timing.commands.isEmpty)