148 add(controls.peer, BorderLayout.NORTH) |
148 add(controls.peer, BorderLayout.NORTH) |
149 |
149 |
150 |
150 |
151 /* component state -- owned by GUI thread */ |
151 /* component state -- owned by GUI thread */ |
152 |
152 |
153 private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing] |
153 private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Node_Timing] |
154 |
154 |
155 private def make_entries(): List[Entry] = |
155 private def make_entries(): List[Entry] = |
156 { |
156 { |
157 GUI_Thread.require {} |
157 GUI_Thread.require {} |
158 |
158 |
159 val name = |
159 val name = |
160 Document_View.get(view.getTextArea) match { |
160 Document_View.get(view.getTextArea) match { |
161 case None => Document.Node.Name.empty |
161 case None => Document.Node.Name.empty |
162 case Some(doc_view) => doc_view.model.node_name |
162 case Some(doc_view) => doc_view.model.node_name |
163 } |
163 } |
164 val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing) |
164 val timing = nodes_timing.getOrElse(name, Document_Status.Node_Timing.empty) |
165 |
165 |
166 val theories = |
166 val theories = |
167 (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.commands.nonEmpty) |
167 (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.commands.nonEmpty) |
168 yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering) |
168 yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering) |
169 val commands = |
169 val commands = |
189 val nodes_timing1 = |
189 val nodes_timing1 = |
190 (nodes_timing /: iterator)({ case (timing1, (name, node)) => |
190 (nodes_timing /: iterator)({ case (timing1, (name, node)) => |
191 if (PIDE.resources.session_base.loaded_theory(name)) timing1 |
191 if (PIDE.resources.session_base.loaded_theory(name)) timing1 |
192 else { |
192 else { |
193 val node_timing = |
193 val node_timing = |
194 Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold) |
194 Document_Status.Node_Timing.make( |
|
195 snapshot.state, snapshot.version, node, timing_threshold) |
195 timing1 + (name -> node_timing) |
196 timing1 + (name -> node_timing) |
196 } |
197 } |
197 }) |
198 }) |
198 nodes_timing = nodes_timing1 |
199 nodes_timing = nodes_timing1 |
199 |
200 |