author | wenzelm |
Sat, 03 Jan 2015 13:11:10 +0100 | |
changeset 59241 | 541b95e94dc7 |
parent 59240 | e411afcfaa29 |
child 59254 | 04f5355f1ab0 |
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 |
|
59227 | 13 |
import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser} |
49730 | 14 |
|
58452 | 15 |
import java.io.{File => JFile} |
16 |
import java.awt.{Color, Dimension, Graphics2D} |
|
49734 | 17 |
import java.awt.geom.Rectangle2D |
18 |
import java.awt.image.BufferedImage |
|
19 |
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
|
20 |
import javax.swing.border.EmptyBorder |
49730 | 21 |
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
|
22 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
23 |
|
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59227
diff
changeset
|
24 |
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
|
25 |
{ |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
26 |
focusable = true |
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
27 |
requestFocus() |
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
28 |
|
59233 | 29 |
val graph_panel = new Graph_Panel(visualizer) |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
30 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
31 |
listenTo(keys) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
32 |
reactions += graph_panel.reactions |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
33 |
|
50475 | 34 |
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
|
35 |
|
50475 | 36 |
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
|
37 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
38 |
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
|
39 |
chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly |
58452 | 40 |
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
|
41 |
|
59227 | 42 |
val options_panel = |
43 |
new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
|
44 |
new CheckBox() { |
|
45 |
selected = visualizer.arrow_heads |
|
46 |
action = Action("Arrow Heads") { |
|
47 |
visualizer.arrow_heads = selected |
|
48 |
graph_panel.repaint() |
|
49 |
} |
|
50 |
}, |
|
51 |
new Button { |
|
52 |
action = Action("Save Image") { |
|
53 |
chooser.showSaveDialog(this) match { |
|
54 |
case FileChooser.Result.Approve => export(chooser.selectedFile) |
|
55 |
case _ => |
|
56 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
57 |
} |
59227 | 58 |
}, |
59 |
graph_panel.zoom, |
|
60 |
new Button { |
|
61 |
action = Action("Apply Layout") { |
|
62 |
graph_panel.apply_layout() |
|
63 |
} |
|
64 |
}, |
|
65 |
new Button { |
|
66 |
action = Action("Fit to Window") { |
|
67 |
graph_panel.fit_to_window() |
|
68 |
} |
|
69 |
}, |
|
70 |
new Button { |
|
71 |
action = Action("Colorations") { |
|
72 |
color_dialog.open |
|
73 |
} |
|
74 |
}, |
|
75 |
new Button { |
|
76 |
action = Action("Filters") { |
|
77 |
mutator_dialog.open |
|
78 |
} |
|
79 |
}) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
80 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
81 |
add(graph_panel, BorderPanel.Position.Center) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
82 |
add(options_panel, BorderPanel.Position.North) |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
83 |
|
58452 | 84 |
private def export(file: JFile) |
85 |
{ |
|
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
86 |
val box = visualizer.Coordinates.bounding_box() |
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
87 |
val w = box.width.ceil.toInt |
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
88 |
val h = box.height.ceil.toInt |
58452 | 89 |
|
90 |
def paint(gfx: Graphics2D) |
|
91 |
{ |
|
92 |
gfx.setColor(Color.WHITE) |
|
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
93 |
gfx.fillRect(0, 0, w, h) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
94 |
|
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
95 |
gfx.translate(- box.x, - box.y) |
58452 | 96 |
visualizer.Drawer.paint_all_visible(gfx, false) |
97 |
} |
|
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
98 |
|
58452 | 99 |
try { |
100 |
val name = file.getName |
|
101 |
if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h) |
|
102 |
else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h) |
|
103 |
else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)") |
|
104 |
} |
|
105 |
catch { |
|
106 |
case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg)) |
|
107 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
108 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
109 |
} |