equal
deleted
inserted
replaced
16 import javax.swing.border.EmptyBorder |
16 import javax.swing.border.EmptyBorder |
17 import java.awt.Dimension |
17 import java.awt.Dimension |
18 import java.io.File |
18 import java.io.File |
19 |
19 |
20 |
20 |
21 class Main_Panel(graph: Model.Graph) extends BorderPanel |
21 class Main_Panel(graph: Model.Graph) |
|
22 extends BorderPanel |
22 { |
23 { |
|
24 def make_tooltip(body: XML.Body): String = |
|
25 { |
|
26 if (body.isEmpty) null |
|
27 else { |
|
28 val txt = Pretty.string_of(body) |
|
29 "<html><pre style=\"font-family: " + Parameters.font_family + "; font-size: " + |
|
30 Parameters.tooltip_font_size + "px; \">" + HTML.encode(txt) + "</pre></html>" |
|
31 } |
|
32 } |
|
33 |
23 focusable = true |
34 focusable = true |
24 requestFocus() |
35 requestFocus() |
25 |
36 |
26 val model = new Model(graph) |
37 val model = new Model(graph) |
27 val visualizer = new Visualizer(model) |
38 val visualizer = new Visualizer(model) |
28 val graph_panel = new Graph_Panel(visualizer) |
39 val graph_panel = new Graph_Panel(visualizer, make_tooltip) |
29 |
40 |
30 listenTo(keys) |
41 listenTo(keys) |
31 reactions += graph_panel.reactions |
42 reactions += graph_panel.reactions |
32 |
43 |
33 val mutator_dialog = new Mutator_Dialog( |
44 val mutator_dialog = new Mutator_Dialog( |