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