equal
deleted
inserted
replaced
103 |
103 |
104 private def handle_update() |
104 private def handle_update() |
105 { |
105 { |
106 GUI_Thread.require {} |
106 GUI_Thread.require {} |
107 |
107 |
108 val new_state = Debugger.current_state() |
|
109 |
|
110 val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot) |
108 val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot) |
111 val new_threads = new_state.threads |
109 val new_threads = Debugger.threads() |
112 val new_output = |
110 val new_output = |
113 { |
111 { |
|
112 val output = Debugger.output() |
114 val current_thread_selection = thread_selection() |
113 val current_thread_selection = thread_selection() |
115 (for { |
114 (for { |
116 (thread_name, results) <- new_state.output |
115 (thread_name, results) <- output |
117 if current_thread_selection.isEmpty || current_thread_selection.get == thread_name |
116 if current_thread_selection.isEmpty || current_thread_selection.get == thread_name |
118 (_, tree) <- results.iterator |
117 (_, tree) <- results.iterator |
119 } yield tree).toList |
118 } yield tree).toList |
120 } |
119 } |
121 |
120 |