changeset 65361 | ecefb68dc21d |
parent 65355 | 403eabd73c9a |
child 65874 | bd45c8ebc214 |
--- a/src/Tools/jEdit/src/timing_dockable.scala Mon Apr 03 16:50:44 2017 +0200 +++ b/src/Tools/jEdit/src/timing_dockable.scala Mon Apr 03 17:00:36 2017 +0200 @@ -187,7 +187,7 @@ } val nodes_timing1 = (nodes_timing /: iterator)({ case (timing1, (name, node)) => - if (PIDE.resources.base.loaded_theory(name)) timing1 + if (PIDE.resources.session_base.loaded_theory(name)) timing1 else { val node_timing = Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)