1/* Title: Tools/Graphview/graph_panel.scala 2 Author: Markus Kaiser, TU Muenchen 3 Author: Makarius 4 5GUI panel for graph layout. 6*/ 7 8package isabelle.graphview 9 10 11import isabelle._ 12 13import java.awt.{Dimension, Graphics2D, Point, Rectangle} 14import java.awt.geom.{AffineTransform, Point2D} 15import javax.imageio.ImageIO 16import javax.swing.{JScrollPane, JComponent, SwingUtilities} 17import javax.swing.border.EmptyBorder 18 19import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser, Panel, ScrollPane} 20import scala.swing.event.{Event, Key, MousePressed, MouseDragged, MouseClicked, MouseEvent} 21 22 23class Graph_Panel(val graphview: Graphview) extends BorderPanel 24{ 25 graph_panel => 26 27 28 29 /** graph **/ 30 31 /* painter */ 32 33 private val painter = new Panel 34 { 35 override def paint(gfx: Graphics2D) 36 { 37 super.paintComponent(gfx) 38 39 gfx.setColor(graphview.background_color) 40 gfx.fillRect(0, 0, peer.getWidth, peer.getHeight) 41 42 gfx.transform(Transform()) 43 graphview.paint(gfx) 44 } 45 } 46 47 def set_preferred_size() 48 { 49 val box = graphview.bounding_box() 50 val s = Transform.scale_discrete 51 painter.preferredSize = new Dimension((box.width * s).ceil.toInt, (box.height * s).ceil.toInt) 52 painter.revalidate() 53 } 54 55 def refresh() 56 { 57 if (painter != null) { 58 set_preferred_size() 59 painter.repaint() 60 } 61 } 62 63 def scroll_to_node(node: Graph_Display.Node) 64 { 65 val gap = graphview.metrics.gap 66 val info = graphview.layout.get_node(node) 67 68 val t = Transform() 69 val p = 70 t.transform(new Point2D.Double(info.x - info.width2 - gap, info.y - info.height2 - gap), null) 71 val q = 72 t.transform(new Point2D.Double(info.x + info.width2 + gap, info.y + info.height2 + gap), null) 73 74 painter.peer.scrollRectToVisible( 75 new Rectangle(p.getX.toInt, p.getY.toInt, 76 (q.getX - p.getX).ceil.toInt, (q.getY - p.getY).ceil.toInt)) 77 } 78 79 80 /* scrollable graph pane */ 81 82 private val graph_pane: ScrollPane = new ScrollPane(painter) { 83 tooltip = "" 84 85 override lazy val peer: JScrollPane = new JScrollPane with SuperMixin { 86 override def getToolTipText(event: java.awt.event.MouseEvent): String = 87 graphview.find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match { 88 case Some(node) => 89 graphview.model.full_graph.get_node(node) match { 90 case Nil => null 91 case content => 92 graphview.make_tooltip(graph_pane.peer, event.getX, event.getY, content) 93 } 94 case None => null 95 } 96 } 97 98 horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always 99 verticalScrollBarPolicy = ScrollPane.BarPolicy.Always 100 101 listenTo(mouse.moves) 102 listenTo(mouse.clicks) 103 reactions += 104 { 105 case MousePressed(_, p, _, _, _) => 106 Mouse_Interaction.pressed(p) 107 painter.repaint() 108 case MouseDragged(_, to, _) => 109 Mouse_Interaction.dragged(to) 110 painter.repaint() 111 case e @ MouseClicked(_, p, m, n, _) => 112 Mouse_Interaction.clicked(p, m, n, SwingUtilities.isRightMouseButton(e.peer)) 113 painter.repaint() 114 } 115 116 contents = painter 117 } 118 graph_pane.peer.getVerticalScrollBar.setUnitIncrement(10) 119 120 121 /* transform */ 122 123 def rescale(s: Double) 124 { 125 Transform.scale = s 126 if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).floor.toInt) 127 refresh() 128 } 129 130 def fit_to_window() 131 { 132 Transform.fit_to_window() 133 refresh() 134 } 135 136 private object Transform 137 { 138 private var _scale: Double = 1.0 139 def scale: Double = _scale 140 def scale_=(s: Double) 141 { 142 _scale = (s min 10.0) max 0.1 143 } 144 145 def scale_discrete: Double = 146 { 147 val font_height = GUI.line_metrics(graphview.metrics.font).getHeight.toInt 148 (scale * font_height).floor / font_height 149 } 150 151 def apply() = 152 { 153 val box = graphview.bounding_box() 154 val t = AffineTransform.getScaleInstance(scale_discrete, scale_discrete) 155 t.translate(- box.x, - box.y) 156 t 157 } 158 159 def fit_to_window() 160 { 161 if (graphview.visible_graph.is_empty) 162 rescale(1.0) 163 else { 164 val box = graphview.bounding_box() 165 rescale((size.width / box.width) min (size.height / box.height)) 166 } 167 } 168 169 def pane_to_graph_coordinates(at: Point2D): Point2D = 170 { 171 val s = Transform.scale_discrete 172 val p = Transform().inverseTransform(graph_pane.peer.getViewport.getViewPosition, null) 173 174 p.setLocation(p.getX + at.getX / s, p.getY + at.getY / s) 175 p 176 } 177 } 178 179 180 /* interaction */ 181 182 graphview.model.Colors.events += { case _ => painter.repaint() } 183 graphview.model.Mutators.events += { case _ => painter.repaint() } 184 185 private object Mouse_Interaction 186 { 187 private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) = 188 (new Point(0, 0), Nil, Nil) 189 190 def pressed(at: Point) 191 { 192 val c = Transform.pane_to_graph_coordinates(at) 193 val l = 194 graphview.find_node(c) match { 195 case Some(node) => 196 if (graphview.Selection.contains(node)) graphview.Selection.get() 197 else List(node) 198 case None => Nil 199 } 200 val d = 201 l match { 202 case Nil => graphview.find_dummy(c).toList 203 case _ => Nil 204 } 205 draginfo = (at, l, d) 206 } 207 208 def dragged(to: Point) 209 { 210 val (from, p, d) = draginfo 211 212 val s = Transform.scale_discrete 213 val dx = to.x - from.x 214 val dy = to.y - from.y 215 216 (p, d) match { 217 case (Nil, Nil) => 218 val r = graph_pane.peer.getViewport.getViewRect 219 r.translate(- dx, - dy) 220 painter.peer.scrollRectToVisible(r) 221 222 case (Nil, ds) => 223 ds.foreach(d => graphview.translate_vertex(d, dx / s, dy / s)) 224 225 case (ls, _) => 226 ls.foreach(l => graphview.translate_vertex(Layout.Node(l), dx / s, dy / s)) 227 } 228 229 draginfo = (to, p, d) 230 } 231 232 def clicked(at: Point, m: Key.Modifiers, clicks: Int, right_click: Boolean) 233 { 234 val c = Transform.pane_to_graph_coordinates(at) 235 236 if (clicks < 2) { 237 if (right_click) { 238 // FIXME 239 if (false) { 240 val menu = Popups(graph_panel, graphview.find_node(c), graphview.Selection.get()) 241 menu.show(graph_pane.peer, at.x, at.y) 242 } 243 } 244 else { 245 (graphview.find_node(c), m) match { 246 case (Some(node), Key.Modifier.Control) => graphview.Selection.add(node) 247 case (None, Key.Modifier.Control) => 248 249 case (Some(node), Key.Modifier.Shift) => graphview.Selection.add(node) 250 case (None, Key.Modifier.Shift) => 251 252 case (Some(node), _) => 253 graphview.Selection.clear() 254 graphview.Selection.add(node) 255 case (None, _) => 256 graphview.Selection.clear() 257 } 258 } 259 } 260 } 261 } 262 263 264 265 /** controls **/ 266 267 private val mutator_dialog = 268 new Mutator_Dialog(graphview, graphview.model.Mutators, "Filters", "Hide", false) 269 private val color_dialog = 270 new Mutator_Dialog(graphview, graphview.model.Colors, "Colorations") 271 272 private val chooser = new FileChooser { 273 fileSelectionMode = FileChooser.SelectionMode.FilesOnly 274 title = "Save image (.png or .pdf)" 275 } 276 277 private val show_content = new CheckBox() { 278 selected = graphview.show_content 279 action = Action("Show content") { 280 graphview.show_content = selected 281 graphview.update_layout() 282 refresh() 283 } 284 tooltip = "Show full node content within graph layout" 285 } 286 287 private val show_arrow_heads = new CheckBox() { 288 selected = graphview.show_arrow_heads 289 action = Action("Show arrow heads") { 290 graphview.show_arrow_heads = selected 291 painter.repaint() 292 } 293 tooltip = "Draw edges with explicit arrow heads" 294 } 295 296 private val show_dummies = new CheckBox() { 297 selected = graphview.show_dummies 298 action = Action("Show dummies") { 299 graphview.show_dummies = selected 300 painter.repaint() 301 } 302 tooltip = "Draw dummy nodes within graph layout, for easier mouse dragging" 303 } 304 305 private val save_image = new Button { 306 action = Action("Save image") { 307 chooser.showSaveDialog(this) match { 308 case FileChooser.Result.Approve => 309 try { Graph_File.write(chooser.selectedFile, graphview) } 310 catch { 311 case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg)) 312 } 313 case _ => 314 } 315 } 316 tooltip = "Save current graph layout as PNG or PDF" 317 } 318 319 private val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) } 320 321 private val fit_window = new Button { 322 action = Action("Fit to window") { fit_to_window() } 323 tooltip = "Zoom to fit window width and height" 324 } 325 326 private val update_layout = new Button { 327 action = Action("Update layout") { 328 graphview.update_layout() 329 refresh() 330 } 331 tooltip = "Regenerate graph layout according to built-in algorithm" 332 } 333 334 private val editor_style = new CheckBox() { 335 selected = graphview.editor_style 336 action = Action("Editor style") { 337 graphview.editor_style = selected 338 graphview.update_layout() 339 refresh() 340 } 341 tooltip = "Use editor font and colors for painting" 342 } 343 344 private val colorations = new Button { action = Action("Colorations") { color_dialog.open } } 345 private val filters = new Button { action = Action("Filters") { mutator_dialog.open } } 346 347 private val controls = 348 Wrap_Panel( 349 List(show_content, show_arrow_heads, show_dummies, 350 save_image, zoom, fit_window, update_layout, editor_style)) // FIXME colorations, filters 351 352 353 354 /** main layout **/ 355 356 layout(graph_pane) = BorderPanel.Position.Center 357 layout(controls) = BorderPanel.Position.North 358 359 rescale(1.0) 360} 361