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}