src/Tools/Graphview/graphview.scala
author wenzelm
Mon Mar 12 11:17:59 2018 +0100 (19 months ago)
changeset 67835 c8e4ee2b5482
parent 67547 aefe7a7b330a
permissions -rw-r--r--
tuned imports;
wenzelm@59459
     1
/*  Title:      Tools/Graphview/graphview.scala
markus@49557
     2
    Author:     Markus Kaiser, TU Muenchen
wenzelm@59240
     3
    Author:     Makarius
markus@49557
     4
wenzelm@59459
     5
Graphview visualization parameters and GUI state.
markus@49557
     6
*/
markus@49557
     7
markus@49557
     8
package isabelle.graphview
markus@49557
     9
wenzelm@50464
    10
wenzelm@49565
    11
import isabelle._
markus@49557
    12
wenzelm@59290
    13
import java.awt.{Font, Color, Shape, Graphics2D}
wenzelm@59305
    14
import java.awt.geom.{Point2D, Rectangle2D}
wenzelm@49729
    15
import javax.swing.JComponent
markus@49557
    16
markus@49557
    17
wenzelm@59462
    18
abstract class Graphview(full_graph: Graph_Display.Graph)
wenzelm@50465
    19
{
wenzelm@59459
    20
  graphview =>
wenzelm@50472
    21
wenzelm@59302
    22
wenzelm@59395
    23
  def options: Options
wenzelm@59392
    24
wenzelm@59462
    25
  val model = new Model(full_graph)
wenzelm@59462
    26
wenzelm@59392
    27
wenzelm@59302
    28
  /* layout state */
wenzelm@59302
    29
wenzelm@59290
    30
  // owned by GUI thread
wenzelm@59303
    31
  private var _layout: Layout = Layout.empty
wenzelm@59303
    32
  def layout: Layout = _layout
wenzelm@59290
    33
wenzelm@59290
    34
  def metrics: Metrics = layout.metrics
wenzelm@59302
    35
  def visible_graph: Graph_Display.Graph = layout.input_graph
wenzelm@59302
    36
wenzelm@59303
    37
  def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit =
wenzelm@59303
    38
    _layout = _layout.translate_vertex(v, dx, dy)
wenzelm@59302
    39
wenzelm@59305
    40
  def find_node(at: Point2D): Option[Graph_Display.Node] =
wenzelm@59305
    41
    layout.output_graph.iterator.collectFirst({
wenzelm@59384
    42
      case (Layout.Node(node), (info, _)) if Shapes.shape(info).contains(at) => node
wenzelm@59305
    43
    })
wenzelm@59305
    44
wenzelm@59305
    45
  def find_dummy(at: Point2D): Option[Layout.Dummy] =
wenzelm@59305
    46
    layout.output_graph.iterator.collectFirst({
wenzelm@59384
    47
      case (dummy: Layout.Dummy, (info, _)) if Shapes.shape(info).contains(at) => dummy
wenzelm@59305
    48
    })
wenzelm@59305
    49
wenzelm@59302
    50
  def bounding_box(): Rectangle2D.Double =
wenzelm@59302
    51
  {
wenzelm@59302
    52
    var x0 = 0.0
wenzelm@59302
    53
    var y0 = 0.0
wenzelm@59302
    54
    var x1 = 0.0
wenzelm@59302
    55
    var y1 = 0.0
wenzelm@59384
    56
    for ((_, (info, _)) <- layout.output_graph.iterator) {
wenzelm@59384
    57
      val rect = Shapes.shape(info)
wenzelm@59384
    58
      x0 = x0 min rect.getMinX
wenzelm@59384
    59
      y0 = y0 min rect.getMinY
wenzelm@59384
    60
      x1 = x1 max rect.getMaxX
wenzelm@59384
    61
      y1 = y1 max rect.getMaxY
wenzelm@59384
    62
    }
wenzelm@59384
    63
    x0 = (x0 - metrics.gap).floor
wenzelm@59384
    64
    y0 = (y0 - metrics.gap).floor
wenzelm@59384
    65
    x1 = (x1 + metrics.gap).ceil
wenzelm@59384
    66
    y1 = (y1 + metrics.gap).ceil
wenzelm@59302
    67
    new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0)
wenzelm@59302
    68
  }
wenzelm@59302
    69
wenzelm@59302
    70
  def update_layout()
wenzelm@59302
    71
  {
wenzelm@59302
    72
    val metrics = Metrics(make_font())
wenzelm@59302
    73
    val visible_graph = model.make_visible_graph()
wenzelm@59302
    74
wenzelm@59384
    75
    def node_text(node: Graph_Display.Node, content: XML.Body): String =
wenzelm@59384
    76
      if (show_content) {
wenzelm@59384
    77
        val s =
wenzelm@67547
    78
          XML.content(Pretty.formatted(content,
wenzelm@67547
    79
            margin = options.int("graphview_content_margin").toDouble,
wenzelm@67547
    80
            metric = metrics.Pretty_Metric))
wenzelm@59384
    81
        if (s.nonEmpty) s else node.toString
wenzelm@59384
    82
      }
wenzelm@59384
    83
      else node.toString
wenzelm@59384
    84
wenzelm@59384
    85
    _layout = Layout.make(options, metrics, node_text _, visible_graph)
wenzelm@59302
    86
  }
wenzelm@59290
    87
wenzelm@50476
    88
wenzelm@59233
    89
  /* tooltips */
wenzelm@59233
    90
wenzelm@59233
    91
  def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
wenzelm@59233
    92
wenzelm@59233
    93
wenzelm@59228
    94
  /* main colors */
wenzelm@59228
    95
wenzelm@59228
    96
  def foreground_color: Color = Color.BLACK
wenzelm@59228
    97
  def background_color: Color = Color.WHITE
wenzelm@61176
    98
  def selection_color: Color = new Color(204, 204, 255)
wenzelm@61176
    99
  def highlight_color: Color = new Color(255, 255, 224)
wenzelm@59228
   100
  def error_color: Color = Color.RED
wenzelm@59251
   101
  def dummy_color: Color = Color.GRAY
wenzelm@59228
   102
wenzelm@59228
   103
wenzelm@50475
   104
  /* font rendering information */
wenzelm@50475
   105
wenzelm@59290
   106
  def make_font(): Font =
wenzelm@59286
   107
  {
wenzelm@59286
   108
    val family = options.string("graphview_font_family")
wenzelm@59286
   109
    val size = options.int("graphview_font_size")
wenzelm@59286
   110
    new Font(family, Font.PLAIN, size)
wenzelm@59286
   111
  }
wenzelm@50475
   112
wenzelm@50475
   113
wenzelm@50475
   114
  /* rendering parameters */
wenzelm@50475
   115
wenzelm@59294
   116
  // owned by GUI thread
wenzelm@59384
   117
  var show_content = false
wenzelm@59384
   118
  var show_arrow_heads = false
wenzelm@59294
   119
  var show_dummies = false
wenzelm@61176
   120
  var editor_style = false
wenzelm@50475
   121
wenzelm@50475
   122
  object Colors
wenzelm@50475
   123
  {
wenzelm@50475
   124
    private val filter_colors = List(
wenzelm@59220
   125
      new Color(0xD9, 0xF2, 0xE2), // blue
wenzelm@59220
   126
      new Color(0xFF, 0xE7, 0xD8), // orange
wenzelm@59220
   127
      new Color(0xFF, 0xFF, 0xE5), // yellow
wenzelm@59220
   128
      new Color(0xDE, 0xCE, 0xFF), // lilac
wenzelm@59220
   129
      new Color(0xCC, 0xEB, 0xFF), // turquoise
wenzelm@59220
   130
      new Color(0xFF, 0xE5, 0xE5), // red
wenzelm@59220
   131
      new Color(0xE5, 0xE5, 0xD9)  // green
wenzelm@50475
   132
    )
wenzelm@50475
   133
wenzelm@50475
   134
    private var curr : Int = -1
wenzelm@59220
   135
    def next(): Color =
wenzelm@50475
   136
    {
wenzelm@50475
   137
      curr = (curr + 1) % filter_colors.length
wenzelm@50475
   138
      filter_colors(curr)
wenzelm@50475
   139
    }
wenzelm@50475
   140
  }
wenzelm@50475
   141
wenzelm@59460
   142
  def paint(gfx: Graphics2D)
wenzelm@59294
   143
  {
wenzelm@59294
   144
    gfx.setRenderingHints(Metrics.rendering_hints)
wenzelm@59410
   145
wenzelm@59459
   146
    for (node <- graphview.current_node)
wenzelm@59459
   147
      Shapes.highlight_node(gfx, graphview, node)
wenzelm@59410
   148
wenzelm@59294
   149
    for (edge <- visible_graph.edges_iterator)
wenzelm@59459
   150
      Shapes.Cardinal_Spline_Edge.paint(gfx, graphview, edge)
wenzelm@59410
   151
wenzelm@59294
   152
    for (node <- visible_graph.keys_iterator)
wenzelm@59459
   153
      Shapes.paint_node(gfx, graphview, node)
wenzelm@59294
   154
  }
wenzelm@50472
   155
wenzelm@59392
   156
  var current_node: Option[Graph_Display.Node] = None
wenzelm@59392
   157
wenzelm@50465
   158
  object Selection
wenzelm@50465
   159
  {
wenzelm@61590
   160
    private val state = Synchronized[List[Graph_Display.Node]](Nil)
wenzelm@50465
   161
wenzelm@59443
   162
    def get(): List[Graph_Display.Node] = state.value
wenzelm@59245
   163
    def contains(node: Graph_Display.Node): Boolean = get().contains(node)
wenzelm@50465
   164
wenzelm@59443
   165
    def add(node: Graph_Display.Node): Unit = state.change(node :: _)
wenzelm@59443
   166
    def clear(): Unit = state.change(_ => Nil)
markus@49557
   167
  }
wenzelm@50465
   168
wenzelm@59220
   169
  sealed case class Node_Color(border: Color, background: Color, foreground: Color)
wenzelm@50464
   170
wenzelm@59245
   171
  def node_color(node: Graph_Display.Node): Node_Color =
wenzelm@59410
   172
    if (Selection.contains(node))
wenzelm@59245
   173
      Node_Color(foreground_color, selection_color, foreground_color)
wenzelm@59410
   174
    else if (current_node == Some(node))
wenzelm@59410
   175
      Node_Color(foreground_color, highlight_color, foreground_color)
wenzelm@59245
   176
    else
wenzelm@59245
   177
      Node_Color(foreground_color, model.colors.getOrElse(node, background_color), foreground_color)
wenzelm@59220
   178
wenzelm@59407
   179
  def edge_color(edge: Graph_Display.Edge, downwards: Boolean): Color =
wenzelm@59407
   180
    if (downwards || show_arrow_heads) foreground_color
wenzelm@59407
   181
    else error_color
markus@49557
   182
}