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