equal
deleted
inserted
replaced
185 case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name))) |
185 case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name))) |
186 case None => snapshot.version.nodes.iterator |
186 case None => snapshot.version.nodes.iterator |
187 } |
187 } |
188 val nodes_timing1 = |
188 val nodes_timing1 = |
189 (nodes_timing /: iterator)({ case (timing1, (name, node)) => |
189 (nodes_timing /: iterator)({ case (timing1, (name, node)) => |
190 if (PIDE.resources.base.loaded_theory(name)) timing1 |
190 if (PIDE.resources.session_base.loaded_theory(name)) timing1 |
191 else { |
191 else { |
192 val node_timing = |
192 val node_timing = |
193 Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold) |
193 Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold) |
194 timing1 + (name -> node_timing) |
194 timing1 + (name -> node_timing) |
195 } |
195 } |