14 MouseEvent, MouseAdapter} |
14 MouseEvent, MouseAdapter} |
15 import javax.swing.{JTree, JMenuItem} |
15 import javax.swing.{JTree, JMenuItem} |
16 import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel} |
16 import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel} |
17 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener} |
17 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener} |
18 |
18 |
|
19 import scala.collection.immutable.SortedMap |
19 import scala.swing.{Button, Label, Component, ScrollPane, SplitPane, Orientation, |
20 import scala.swing.{Button, Label, Component, ScrollPane, SplitPane, Orientation, |
20 CheckBox, BorderPanel} |
21 CheckBox, BorderPanel} |
21 import scala.swing.event.ButtonClicked |
22 import scala.swing.event.ButtonClicked |
22 |
23 |
23 import org.gjt.sp.jedit.{jEdit, View} |
24 import org.gjt.sp.jedit.{jEdit, View} |
68 |
69 |
69 |
70 |
70 /* component state -- owned by GUI thread */ |
71 /* component state -- owned by GUI thread */ |
71 |
72 |
72 private var current_snapshot = Document.Snapshot.init |
73 private var current_snapshot = Document.Snapshot.init |
73 private var current_threads: Map[String, List[Debugger.Debug_State]] = Map.empty |
74 private var current_threads: Debugger.Threads = SortedMap.empty |
74 private var current_output: List[XML.Tree] = Nil |
75 private var current_output: List[XML.Tree] = Nil |
75 |
76 |
76 |
77 |
77 /* pretty text area */ |
78 /* pretty text area */ |
78 |
79 |
106 } |
107 } |
107 |
108 |
108 if (new_threads != current_threads) { |
109 if (new_threads != current_threads) { |
109 val threads = |
110 val threads = |
110 (for ((a, b) <- new_threads.iterator) |
111 (for ((a, b) <- new_threads.iterator) |
111 yield Debugger.Context(a, b)).toList.sortBy(_.thread_name) |
112 yield Debugger.Context(a, b)).toList |
112 update_tree(threads) |
113 update_tree(threads) |
113 } |
114 } |
114 |
115 |
115 if (new_output != current_output) |
116 if (new_output != current_output) |
116 pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output)) |
117 pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output)) |