author | wenzelm |
Mon, 19 Jan 2015 16:31:04 +0100 | |
changeset 59406 | 283aa6225d98 |
parent 59400 | d833cba5cce5 |
child 59408 | 63cb603b5114 |
permissions | -rw-r--r-- |
59202 | 1 |
/* Title: Tools/Graphview/main_panel.scala |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Markus Kaiser, TU Muenchen |
59240 | 3 |
Author: Makarius |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
4 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
5 |
Graph Panel wrapper. |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
6 |
*/ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
7 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
8 |
package isabelle.graphview |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
9 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
10 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
11 |
import isabelle._ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
12 |
|
59392 | 13 |
import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser, SplitPane, Orientation} |
49730 | 14 |
|
58452 | 15 |
import java.io.{File => JFile} |
59289 | 16 |
import java.awt.{Color, Graphics2D} |
49734 | 17 |
import javax.imageio.ImageIO |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
18 |
import javax.swing.border.EmptyBorder |
49730 | 19 |
import javax.swing.JComponent |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
20 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
21 |
|
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59227
diff
changeset
|
22 |
class Main_Panel(model: Model, visualizer: Visualizer) extends BorderPanel |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
23 |
{ |
59233 | 24 |
val graph_panel = new Graph_Panel(visualizer) |
59397 | 25 |
val tree_panel = new Tree_Panel(visualizer, graph_panel) |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
26 |
|
59392 | 27 |
def update_layout() |
28 |
{ |
|
29 |
visualizer.update_layout() |
|
30 |
tree_panel.refresh() |
|
31 |
graph_panel.refresh() |
|
32 |
} |
|
33 |
||
59393 | 34 |
val split_pane = |
59395 | 35 |
if (visualizer.options.bool("graphview_swap_panels")) |
59393 | 36 |
new SplitPane(Orientation.Vertical, tree_panel, graph_panel) |
37 |
else |
|
38 |
new SplitPane(Orientation.Vertical, graph_panel, tree_panel) |
|
59392 | 39 |
split_pane.oneTouchExpandable = true |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
40 |
|
50475 | 41 |
val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
42 |
|
50475 | 43 |
val color_dialog = new Mutator_Dialog(visualizer, model.Colors, "Colorations") |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
44 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
45 |
private val chooser = new FileChooser() |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
46 |
chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly |
59254 | 47 |
chooser.title = "Save image (.png or .pdf)" |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
48 |
|
59392 | 49 |
val controls = |
59227 | 50 |
new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
51 |
new CheckBox() { |
|
59384 | 52 |
selected = visualizer.show_content |
53 |
action = Action("Show content") { |
|
54 |
visualizer.show_content = selected |
|
59392 | 55 |
update_layout() |
59384 | 56 |
} |
59406
283aa6225d98
proper tooltips -- override action toolTip which is empty here;
wenzelm
parents:
59400
diff
changeset
|
57 |
tooltip = "Show full node content within graph layout" |
59384 | 58 |
}, |
59 |
new CheckBox() { |
|
60 |
selected = visualizer.show_arrow_heads |
|
61 |
action = Action("Show arrow heads") { |
|
62 |
visualizer.show_arrow_heads = selected |
|
59396 | 63 |
graph_panel.repaint() |
59384 | 64 |
} |
59406
283aa6225d98
proper tooltips -- override action toolTip which is empty here;
wenzelm
parents:
59400
diff
changeset
|
65 |
tooltip = "Draw edges with explicit arrow heads" |
59227 | 66 |
}, |
59294 | 67 |
new CheckBox() { |
68 |
selected = visualizer.show_dummies |
|
59384 | 69 |
action = Action("Show dummies") { |
70 |
visualizer.show_dummies = selected |
|
59396 | 71 |
graph_panel.repaint() |
59384 | 72 |
} |
59406
283aa6225d98
proper tooltips -- override action toolTip which is empty here;
wenzelm
parents:
59400
diff
changeset
|
73 |
tooltip = "Draw dummy nodes within graph layout, for easier mouse dragging" |
59294 | 74 |
}, |
59227 | 75 |
new Button { |
59254 | 76 |
action = Action("Save image") { |
59227 | 77 |
chooser.showSaveDialog(this) match { |
78 |
case FileChooser.Result.Approve => export(chooser.selectedFile) |
|
79 |
case _ => |
|
80 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
81 |
} |
59406
283aa6225d98
proper tooltips -- override action toolTip which is empty here;
wenzelm
parents:
59400
diff
changeset
|
82 |
tooltip = "Save current graph layout as PNG or PDF" |
59227 | 83 |
}, |
84 |
graph_panel.zoom, |
|
59406
283aa6225d98
proper tooltips -- override action toolTip which is empty here;
wenzelm
parents:
59400
diff
changeset
|
85 |
new Button { |
283aa6225d98
proper tooltips -- override action toolTip which is empty here;
wenzelm
parents:
59400
diff
changeset
|
86 |
action = Action("Fit to window") { graph_panel.fit_to_window() } |
283aa6225d98
proper tooltips -- override action toolTip which is empty here;
wenzelm
parents:
59400
diff
changeset
|
87 |
tooltip = "Zoom to fit window width and height" |
283aa6225d98
proper tooltips -- override action toolTip which is empty here;
wenzelm
parents:
59400
diff
changeset
|
88 |
}, |
283aa6225d98
proper tooltips -- override action toolTip which is empty here;
wenzelm
parents:
59400
diff
changeset
|
89 |
new Button { |
283aa6225d98
proper tooltips -- override action toolTip which is empty here;
wenzelm
parents:
59400
diff
changeset
|
90 |
action = Action("Update layout") { update_layout() } |
283aa6225d98
proper tooltips -- override action toolTip which is empty here;
wenzelm
parents:
59400
diff
changeset
|
91 |
tooltip = "Regenerate graph layout according to built-in algorithm" |
283aa6225d98
proper tooltips -- override action toolTip which is empty here;
wenzelm
parents:
59400
diff
changeset
|
92 |
}) |
59400 | 93 |
/* FIXME |
59254 | 94 |
new Button { action = Action("Colorations") { color_dialog.open } }, |
59400 | 95 |
new Button { action = Action("Filters") { mutator_dialog.open } } |
96 |
*/ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
97 |
|
59392 | 98 |
layout(split_pane) = BorderPanel.Position.Center |
99 |
layout(controls) = BorderPanel.Position.North |
|
100 |
update_layout() |
|
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
101 |
|
58452 | 102 |
private def export(file: JFile) |
103 |
{ |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
104 |
val box = visualizer.bounding_box() |
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
105 |
val w = box.width.ceil.toInt |
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
106 |
val h = box.height.ceil.toInt |
58452 | 107 |
|
108 |
def paint(gfx: Graphics2D) |
|
109 |
{ |
|
110 |
gfx.setColor(Color.WHITE) |
|
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
111 |
gfx.fillRect(0, 0, w, h) |
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
112 |
gfx.translate(- box.x, - box.y) |
59294 | 113 |
visualizer.paint_all_visible(gfx) |
58452 | 114 |
} |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
115 |
|
58452 | 116 |
try { |
117 |
val name = file.getName |
|
118 |
if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h) |
|
119 |
else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h) |
|
120 |
else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)") |
|
121 |
} |
|
122 |
catch { |
|
123 |
case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg)) |
|
124 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
125 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
126 |
} |