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