src/Tools/Graphview/graph_panel.scala
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 66206 2d2082db735a
permissions -rw-r--r--
more strict AFP properties;
     1 /*  Title:      Tools/Graphview/graph_panel.scala
     2     Author:     Markus Kaiser, TU Muenchen
     3     Author:     Makarius
     4 
     5 GUI panel for graph layout.
     6 */
     7 
     8 package isabelle.graphview
     9 
    10 
    11 import isabelle._
    12 
    13 import java.awt.{Dimension, Graphics2D, Point, Rectangle}
    14 import java.awt.geom.{AffineTransform, Point2D}
    15 import javax.imageio.ImageIO
    16 import javax.swing.{JScrollPane, JComponent, SwingUtilities}
    17 import javax.swing.border.EmptyBorder
    18 
    19 import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser, Panel, ScrollPane}
    20 import scala.swing.event.{Event, Key, MousePressed, MouseDragged, MouseClicked, MouseEvent}
    21 
    22 
    23 class 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 }