--- a/src/Tools/jEdit/src/timing_dockable.scala Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Thu Mar 04 15:41:46 2021 +0100
@@ -186,9 +186,8 @@
(restriction match {
case Some(names) => names.iterator.map(name => (name, snapshot.get_node(name)))
case None => snapshot.version.nodes.iterator
- })
- .foldLeft(nodes_timing)(
- { case (timing1, (name, node)) =>
+ }).foldLeft(nodes_timing) {
+ case (timing1, (name, node)) =>
if (PIDE.resources.session_base.loaded_theory(name)) timing1
else {
val node_timing =
@@ -196,7 +195,7 @@
snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
timing1 + (name -> node_timing)
}
- })
+ }
nodes_timing = nodes_timing1
val entries = make_entries()