1 /* Title: Tools/Graphview/src/main_panel.scala |
|
2 Author: Markus Kaiser, TU Muenchen |
|
3 |
|
4 Graph Panel wrapper. |
|
5 */ |
|
6 |
|
7 package isabelle.graphview |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 import isabelle.graphview.Mutators._ |
|
12 |
|
13 import scala.collection.JavaConversions._ |
|
14 import scala.swing.{BorderPanel, Button, BoxPanel, |
|
15 Orientation, Swing, CheckBox, Action, FileChooser} |
|
16 |
|
17 import java.io.{File => JFile} |
|
18 import java.awt.{Color, Dimension, Graphics2D} |
|
19 import java.awt.geom.Rectangle2D |
|
20 import java.awt.image.BufferedImage |
|
21 import javax.imageio.ImageIO |
|
22 import javax.swing.border.EmptyBorder |
|
23 import javax.swing.JComponent |
|
24 |
|
25 |
|
26 class Main_Panel(graph: Model.Graph) extends BorderPanel |
|
27 { |
|
28 focusable = true |
|
29 requestFocus() |
|
30 |
|
31 val model = new Model(graph) |
|
32 val visualizer = new Visualizer(model) |
|
33 |
|
34 def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null |
|
35 val graph_panel = new Graph_Panel(visualizer, make_tooltip) |
|
36 |
|
37 listenTo(keys) |
|
38 reactions += graph_panel.reactions |
|
39 |
|
40 val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false) |
|
41 |
|
42 val color_dialog = new Mutator_Dialog(visualizer, model.Colors, "Colorations") |
|
43 |
|
44 private val chooser = new FileChooser() |
|
45 chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly |
|
46 chooser.title = "Save Image (.png or .pdf)" |
|
47 |
|
48 val options_panel = new BoxPanel(Orientation.Horizontal) { |
|
49 border = new EmptyBorder(0, 0, 10, 0) |
|
50 |
|
51 contents += Swing.HGlue |
|
52 contents += new CheckBox(){ |
|
53 selected = visualizer.arrow_heads |
|
54 action = Action("Arrow Heads"){ |
|
55 visualizer.arrow_heads = selected |
|
56 graph_panel.repaint() |
|
57 } |
|
58 } |
|
59 contents += Swing.RigidBox(new Dimension(10, 0)) |
|
60 contents += new Button{ |
|
61 action = Action("Save Image"){ |
|
62 chooser.showSaveDialog(this) match { |
|
63 case FileChooser.Result.Approve => export(chooser.selectedFile) |
|
64 case _ => |
|
65 } |
|
66 } |
|
67 } |
|
68 contents += Swing.RigidBox(new Dimension(10, 0)) |
|
69 contents += graph_panel.zoom |
|
70 |
|
71 contents += Swing.RigidBox(new Dimension(10, 0)) |
|
72 contents += new Button{ |
|
73 action = Action("Apply Layout"){ |
|
74 graph_panel.apply_layout() |
|
75 } |
|
76 } |
|
77 contents += Swing.RigidBox(new Dimension(10, 0)) |
|
78 contents += new Button{ |
|
79 action = Action("Fit to Window"){ |
|
80 graph_panel.fit_to_window() |
|
81 } |
|
82 } |
|
83 contents += Swing.RigidBox(new Dimension(10, 0)) |
|
84 contents += new Button{ |
|
85 action = Action("Colorations"){ |
|
86 color_dialog.open |
|
87 } |
|
88 } |
|
89 contents += Swing.RigidBox(new Dimension(10, 0)) |
|
90 contents += new Button{ |
|
91 action = Action("Filters"){ |
|
92 mutator_dialog.open |
|
93 } |
|
94 } |
|
95 } |
|
96 |
|
97 add(graph_panel, BorderPanel.Position.Center) |
|
98 add(options_panel, BorderPanel.Position.North) |
|
99 |
|
100 private def export(file: JFile) |
|
101 { |
|
102 val (x0, y0, x1, y1) = visualizer.Coordinates.bounds |
|
103 val w = (math.abs(x1 - x0) + 400).toInt |
|
104 val h = (math.abs(y1 - y0) + 200).toInt |
|
105 |
|
106 def paint(gfx: Graphics2D) |
|
107 { |
|
108 gfx.setColor(Color.WHITE) |
|
109 gfx.fill(new Rectangle2D.Double(0, 0, w, h)) |
|
110 |
|
111 gfx.translate(- x0 + 200, - y0 + 100) |
|
112 visualizer.Drawer.paint_all_visible(gfx, false) |
|
113 } |
|
114 |
|
115 try { |
|
116 val name = file.getName |
|
117 if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h) |
|
118 else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h) |
|
119 else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)") |
|
120 } |
|
121 catch { |
|
122 case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg)) |
|
123 } |
|
124 } |
|
125 } |
|