--- a/src/Tools/jEdit/src/timing_dockable.scala Wed Mar 03 22:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Wed Mar 03 22:48:46 2021 +0100
@@ -182,21 +182,21 @@
val snapshot = PIDE.session.snapshot()
- val iterator =
- restriction match {
+ val nodes_timing1 =
+ (restriction match {
case Some(names) => names.iterator.map(name => (name, snapshot.get_node(name)))
case None => snapshot.version.nodes.iterator
- }
- val nodes_timing1 =
- (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
- if (PIDE.resources.session_base.loaded_theory(name)) timing1
- else {
- val node_timing =
- Document_Status.Overall_Timing.make(
- snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
- timing1 + (name -> node_timing)
- }
})
+ .foldLeft(nodes_timing)(
+ { case (timing1, (name, node)) =>
+ if (PIDE.resources.session_base.loaded_theory(name)) timing1
+ else {
+ val node_timing =
+ Document_Status.Overall_Timing.make(
+ snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
+ timing1 + (name -> node_timing)
+ }
+ })
nodes_timing = nodes_timing1
val entries = make_entries()