31 |
31 |
32 val model = new Model(graph) |
32 val model = new Model(graph) |
33 val visualizer = new Visualizer(model) |
33 val visualizer = new Visualizer(model) |
34 |
34 |
35 def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = |
35 def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = |
36 "<html><pre style=\"font-family: " + visualizer.parameters.font_family + |
36 "<html><pre style=\"font-family: " + visualizer.font_family + |
37 "; font-size: " + visualizer.parameters.tooltip_font_size + "px; \">" + |
37 "; font-size: " + visualizer.tooltip_font_size + "px; \">" + |
38 HTML.encode(Pretty.string_of(body)) + "</pre></html>" |
38 HTML.encode(Pretty.string_of(body)) + "</pre></html>" |
39 |
39 |
40 val graph_panel = new Graph_Panel(visualizer, make_tooltip) |
40 val graph_panel = new Graph_Panel(visualizer, make_tooltip) |
41 |
41 |
42 listenTo(keys) |
42 listenTo(keys) |
43 reactions += graph_panel.reactions |
43 reactions += graph_panel.reactions |
44 |
44 |
45 val mutator_dialog = |
45 val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false) |
46 new Mutator_Dialog(visualizer.parameters, model.Mutators, "Filters", "Hide", false) |
|
47 |
46 |
48 val color_dialog = new Mutator_Dialog(visualizer.parameters, model.Colors, "Colorations") |
47 val color_dialog = new Mutator_Dialog(visualizer, model.Colors, "Colorations") |
49 |
48 |
50 private val chooser = new FileChooser() |
49 private val chooser = new FileChooser() |
51 chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly |
50 chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly |
52 chooser.title = "Graph export" |
51 chooser.title = "Graph export" |
53 |
52 |
54 val options_panel = new BoxPanel(Orientation.Horizontal) { |
53 val options_panel = new BoxPanel(Orientation.Horizontal) { |
55 border = new EmptyBorder(0, 0, 10, 0) |
54 border = new EmptyBorder(0, 0, 10, 0) |
56 |
55 |
57 contents += Swing.HGlue |
56 contents += Swing.HGlue |
58 contents += new CheckBox(){ |
57 contents += new CheckBox(){ |
59 selected = visualizer.parameters.arrow_heads |
58 selected = visualizer.arrow_heads |
60 action = Action("Arrow Heads"){ |
59 action = Action("Arrow Heads"){ |
61 visualizer.parameters.arrow_heads = selected |
60 visualizer.arrow_heads = selected |
62 graph_panel.repaint() |
61 graph_panel.repaint() |
63 } |
62 } |
64 } |
63 } |
65 contents += Swing.RigidBox(new Dimension(10, 0)) |
64 contents += Swing.RigidBox(new Dimension(10, 0)) |
66 contents += new Button{ |
65 contents += new Button{ |