equal
deleted
inserted
replaced
23 class Main_Panel(model: Model, visualizer: Visualizer) extends BorderPanel |
23 class Main_Panel(model: Model, visualizer: Visualizer) extends BorderPanel |
24 { |
24 { |
25 focusable = true |
25 focusable = true |
26 requestFocus() |
26 requestFocus() |
27 |
27 |
28 def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null |
28 val graph_panel = new Graph_Panel(visualizer) |
29 val graph_panel = new Graph_Panel(visualizer, make_tooltip) |
|
30 |
29 |
31 listenTo(keys) |
30 listenTo(keys) |
32 reactions += graph_panel.reactions |
31 reactions += graph_panel.reactions |
33 |
32 |
34 val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false) |
33 val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false) |