1/* Title: Tools/Graphview/shapes.scala 2 Author: Markus Kaiser, TU Muenchen 3 Author: Makarius 4 5Drawable shapes. 6*/ 7 8package isabelle.graphview 9 10 11import isabelle._ 12 13import java.awt.{BasicStroke, Graphics2D, Shape} 14import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, 15 RoundRectangle2D, PathIterator} 16 17 18object Shapes 19{ 20 private val default_stroke = 21 new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) 22 23 def shape(info: Layout.Info): Rectangle2D.Double = 24 new Rectangle2D.Double(info.x - info.width2, info.y - info.height2, info.width, info.height) 25 26 def highlight_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node) 27 { 28 val metrics = graphview.metrics 29 val extra = metrics.char_width 30 val info = graphview.layout.get_node(node) 31 32 gfx.setColor(graphview.highlight_color) 33 gfx.fill(new Rectangle2D.Double( 34 info.x - info.width2 - extra, 35 info.y - info.height2 - extra, 36 info.width + 2 * extra, 37 info.height + 2 * extra)) 38 } 39 40 def paint_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node) 41 { 42 val metrics = graphview.metrics 43 val info = graphview.layout.get_node(node) 44 val c = graphview.node_color(node) 45 val s = shape(info) 46 47 gfx.setColor(c.background) 48 gfx.fill(s) 49 50 gfx.setColor(c.border) 51 gfx.setStroke(default_stroke) 52 gfx.draw(s) 53 54 gfx.setColor(c.foreground) 55 gfx.setFont(metrics.font) 56 57 val text_width = 58 (0.0 /: info.lines) { case (w, line) => w max metrics.string_bounds(line).getWidth } 59 val text_height = 60 (info.lines.length max 1) * metrics.height.ceil 61 val x = (s.getCenterX - text_width / 2).round.toInt 62 var y = (s.getCenterY - text_height / 2 + metrics.ascent).round.toInt 63 for (line <- info.lines) { 64 gfx.drawString(Word.bidi_override(line), x, y) 65 y += metrics.height.ceil.toInt 66 } 67 } 68 69 def paint_dummy(gfx: Graphics2D, graphview: Graphview, info: Layout.Info) 70 { 71 gfx.setStroke(default_stroke) 72 gfx.setColor(graphview.dummy_color) 73 gfx.draw(shape(info)) 74 } 75 76 object Straight_Edge 77 { 78 def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge) 79 { 80 val p = graphview.layout.get_node(edge._1) 81 val q = graphview.layout.get_node(edge._2) 82 val ds = 83 { 84 val a = p.y min q.y 85 val b = p.y max q.y 86 graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList 87 } 88 val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) 89 90 path.moveTo(p.x, p.y) 91 ds.foreach(d => path.lineTo(d.x, d.y)) 92 path.lineTo(q.x, q.y) 93 94 if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _)) 95 96 gfx.setStroke(default_stroke) 97 gfx.setColor(graphview.edge_color(edge, p.y < q.y)) 98 gfx.draw(path) 99 100 if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q)) 101 } 102 } 103 104 object Cardinal_Spline_Edge 105 { 106 private val slack = 0.1 107 108 def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge) 109 { 110 val p = graphview.layout.get_node(edge._1) 111 val q = graphview.layout.get_node(edge._2) 112 val ds = 113 { 114 val a = p.y min q.y 115 val b = p.y max q.y 116 graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList 117 } 118 119 if (ds.isEmpty) Straight_Edge.paint(gfx, graphview, edge) 120 else { 121 val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) 122 path.moveTo(p.x, p.y) 123 124 val coords = p :: ds ::: List(q) 125 val dx = coords(2).x - coords(0).x 126 val dy = coords(2).y - coords(0).y 127 128 val (dx2, dy2) = 129 ((dx, dy) /: coords.sliding(3)) { 130 case ((dx, dy), List(l, m, r)) => 131 val dx2 = r.x - l.x 132 val dy2 = r.y - l.y 133 path.curveTo( 134 l.x + slack * dx, l.y + slack * dy, 135 m.x - slack * dx2, m.y - slack * dy2, 136 m.x, m.y) 137 (dx2, dy2) 138 } 139 140 val l = ds.last 141 path.curveTo( 142 l.x + slack * dx2, l.y + slack * dy2, 143 q.x - slack * dx2, q.y - slack * dy2, 144 q.x, q.y) 145 146 if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _)) 147 148 gfx.setStroke(default_stroke) 149 gfx.setColor(graphview.edge_color(edge, p.y < q.y)) 150 gfx.draw(path) 151 152 if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q)) 153 } 154 } 155 } 156 157 object Arrow_Head 158 { 159 type Point = (Double, Double) 160 161 private def position(path: GeneralPath, shape: Shape): Option[AffineTransform] = 162 { 163 def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] = 164 { 165 val i = path.getPathIterator(null, 1.0) 166 val seg = Array[Double](0.0, 0.0, 0.0, 0.0, 0.0, 0.0) 167 var p1 = (0.0, 0.0) 168 var p2 = (0.0, 0.0) 169 while (!i.isDone) { 170 i.currentSegment(seg) match { 171 case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1)) 172 case PathIterator.SEG_LINETO => 173 p1 = p2 174 p2 = (seg(0), seg(1)) 175 176 if(shape.contains(seg(0), seg(1))) 177 return Some((p1, p2)) 178 case _ => 179 } 180 i.next() 181 } 182 None 183 } 184 185 def binary_search(line: (Point, Point), shape: Shape): Option[AffineTransform] = 186 { 187 val ((fx, fy), (tx, ty)) = line 188 if (shape.contains(fx, fy) == shape.contains(tx, ty)) 189 None 190 else { 191 val (dx, dy) = (fx - tx, fy - ty) 192 if ((dx * dx + dy * dy) < 1.0) { 193 val at = AffineTransform.getTranslateInstance(fx, fy) 194 at.rotate(- (math.atan2(dx, dy) + math.Pi / 2)) 195 Some(at) 196 } 197 else { 198 val (mx, my) = (fx + (tx - fx) / 2.0, fy + (ty - fy) / 2.0) 199 if (shape.contains(fx, fy) == shape.contains(mx, my)) 200 binary_search(((mx, my), (tx, ty)), shape) 201 else 202 binary_search(((fx, fy), (mx, my)), shape) 203 } 204 } 205 } 206 207 intersecting_line(path, shape) match { 208 case None => None 209 case Some(line) => binary_search(line, shape) 210 } 211 } 212 213 def paint(gfx: Graphics2D, path: GeneralPath, shape: Shape) 214 { 215 position(path, shape) match { 216 case None => 217 case Some(at) => 218 val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3) 219 arrow.moveTo(0, 0) 220 arrow.lineTo(-10, 4) 221 arrow.lineTo(-6, 0) 222 arrow.lineTo(-10, -4) 223 arrow.lineTo(0, 0) 224 arrow.transform(at) 225 gfx.fill(arrow) 226 } 227 } 228 } 229} 230