1 /* Title: Tools/Graphview/src/shapes.scala |
|
2 Author: Markus Kaiser, TU Muenchen |
|
3 |
|
4 Drawable shapes. |
|
5 */ |
|
6 |
|
7 package isabelle.graphview |
|
8 |
|
9 |
|
10 import java.awt.{BasicStroke, Graphics2D, Shape} |
|
11 import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, PathIterator} |
|
12 |
|
13 |
|
14 object Shapes |
|
15 { |
|
16 trait Node |
|
17 { |
|
18 def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape |
|
19 def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit |
|
20 } |
|
21 |
|
22 object Growing_Node extends Node |
|
23 { |
|
24 private val stroke = |
|
25 new BasicStroke(3, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) |
|
26 |
|
27 def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Rectangle2D.Double = |
|
28 { |
|
29 val (x, y) = visualizer.Coordinates(peer.get) |
|
30 val bounds = g.getFontMetrics.getStringBounds(visualizer.Caption(peer.get), g) |
|
31 val w = bounds.getWidth + visualizer.pad_x |
|
32 val h = bounds.getHeight + visualizer.pad_y |
|
33 new Rectangle2D.Double(x - (w / 2), y - (h / 2), w, h) |
|
34 } |
|
35 |
|
36 def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]) |
|
37 { |
|
38 val caption = visualizer.Caption(peer.get) |
|
39 val bounds = g.getFontMetrics.getStringBounds(caption, g) |
|
40 val s = shape(g, visualizer, peer) |
|
41 |
|
42 val (border, background, foreground) = visualizer.Color(peer) |
|
43 g.setStroke(stroke) |
|
44 g.setColor(border) |
|
45 g.draw(s) |
|
46 g.setColor(background) |
|
47 g.fill(s) |
|
48 g.setColor(foreground) |
|
49 g.drawString(caption, |
|
50 (s.getCenterX + (- bounds.getWidth / 2)).toFloat, |
|
51 (s.getCenterY + 5).toFloat) |
|
52 } |
|
53 } |
|
54 |
|
55 object Dummy extends Node |
|
56 { |
|
57 private val stroke = |
|
58 new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) |
|
59 private val shape = new Rectangle2D.Double(-5, -5, 10, 10) |
|
60 private val identity = new AffineTransform() |
|
61 |
|
62 def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape = shape |
|
63 |
|
64 def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit = |
|
65 paint_transformed(g, visualizer, peer, identity) |
|
66 |
|
67 def paint_transformed(g: Graphics2D, visualizer: Visualizer, |
|
68 peer: Option[String], at: AffineTransform) |
|
69 { |
|
70 val (border, background, foreground) = visualizer.Color(peer) |
|
71 g.setStroke(stroke) |
|
72 g.setColor(border) |
|
73 g.draw(at.createTransformedShape(shape)) |
|
74 } |
|
75 } |
|
76 |
|
77 trait Edge |
|
78 { |
|
79 def paint(g: Graphics2D, visualizer: Visualizer, |
|
80 peer: (String, String), head: Boolean, dummies: Boolean) |
|
81 } |
|
82 |
|
83 object Straight_Edge extends Edge |
|
84 { |
|
85 private val stroke = |
|
86 new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) |
|
87 |
|
88 def paint(g: Graphics2D, visualizer: Visualizer, |
|
89 peer: (String, String), head: Boolean, dummies: Boolean) |
|
90 { |
|
91 val ((fx, fy), (tx, ty)) = (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2)) |
|
92 val ds = |
|
93 { |
|
94 val min = fy min ty |
|
95 val max = fy max ty |
|
96 visualizer.Coordinates(peer).filter({ case (_, y) => y > min && y < max }) |
|
97 } |
|
98 val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) |
|
99 |
|
100 path.moveTo(fx, fy) |
|
101 ds.foreach({case (x, y) => path.lineTo(x, y)}) |
|
102 path.lineTo(tx, ty) |
|
103 |
|
104 if (dummies) { |
|
105 ds.foreach({ |
|
106 case (x, y) => { |
|
107 val at = AffineTransform.getTranslateInstance(x, y) |
|
108 Dummy.paint_transformed(g, visualizer, None, at) |
|
109 } |
|
110 }) |
|
111 } |
|
112 |
|
113 g.setStroke(stroke) |
|
114 g.setColor(visualizer.Color(peer)) |
|
115 g.draw(path) |
|
116 |
|
117 if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2))) |
|
118 } |
|
119 } |
|
120 |
|
121 object Cardinal_Spline_Edge extends Edge |
|
122 { |
|
123 private val stroke = |
|
124 new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) |
|
125 private val slack = 0.1 |
|
126 |
|
127 def paint(g: Graphics2D, visualizer: Visualizer, |
|
128 peer: (String, String), head: Boolean, dummies: Boolean) |
|
129 { |
|
130 val ((fx, fy), (tx, ty)) = |
|
131 (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2)) |
|
132 val ds = |
|
133 { |
|
134 val min = fy min ty |
|
135 val max = fy max ty |
|
136 visualizer.Coordinates(peer).filter({case (_, y) => y > min && y < max}) |
|
137 } |
|
138 |
|
139 if (ds.isEmpty) Straight_Edge.paint(g, visualizer, peer, head, dummies) |
|
140 else { |
|
141 val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) |
|
142 path.moveTo(fx, fy) |
|
143 |
|
144 val coords = ((fx, fy) :: ds ::: List((tx, ty))) |
|
145 val (dx, dy) = (coords(2)._1 - coords(0)._1, coords(2)._2 - coords(0)._2) |
|
146 |
|
147 val (dx2, dy2) = |
|
148 ((dx, dy) /: coords.sliding(3))({ |
|
149 case ((dx, dy), List((lx, ly), (mx, my), (rx, ry))) => { |
|
150 val (dx2, dy2) = (rx - lx, ry - ly) |
|
151 |
|
152 path.curveTo(lx + slack * dx , ly + slack * dy, |
|
153 mx - slack * dx2, my - slack * dy2, |
|
154 mx , my) |
|
155 (dx2, dy2) |
|
156 } |
|
157 }) |
|
158 |
|
159 val (lx, ly) = ds.last |
|
160 path.curveTo(lx + slack * dx2, ly + slack * dy2, |
|
161 tx - slack * dx2, ty - slack * dy2, |
|
162 tx , ty) |
|
163 |
|
164 if (dummies) { |
|
165 ds.foreach({ |
|
166 case (x, y) => { |
|
167 val at = AffineTransform.getTranslateInstance(x, y) |
|
168 Dummy.paint_transformed(g, visualizer, None, at) |
|
169 } |
|
170 }) |
|
171 } |
|
172 |
|
173 g.setStroke(stroke) |
|
174 g.setColor(visualizer.Color(peer)) |
|
175 g.draw(path) |
|
176 |
|
177 if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2))) |
|
178 } |
|
179 } |
|
180 } |
|
181 |
|
182 object Arrow_Head |
|
183 { |
|
184 type Point = (Double, Double) |
|
185 |
|
186 private def position(path: GeneralPath, shape: Shape): Option[AffineTransform] = |
|
187 { |
|
188 def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] = |
|
189 { |
|
190 val i = path.getPathIterator(null, 1.0) |
|
191 val seg = Array[Double](0,0,0,0,0,0) |
|
192 var p1 = (0.0, 0.0) |
|
193 var p2 = (0.0, 0.0) |
|
194 while (!i.isDone()) { |
|
195 i.currentSegment(seg) match { |
|
196 case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1)) |
|
197 case PathIterator.SEG_LINETO => |
|
198 p1 = p2 |
|
199 p2 = (seg(0), seg(1)) |
|
200 |
|
201 if(shape.contains(seg(0), seg(1))) |
|
202 return Some((p1, p2)) |
|
203 case _ => |
|
204 } |
|
205 i.next() |
|
206 } |
|
207 None |
|
208 } |
|
209 |
|
210 def binary_search(line: (Point, Point), shape: Shape): Option[AffineTransform] = |
|
211 { |
|
212 val ((fx, fy), (tx, ty)) = line |
|
213 if (shape.contains(fx, fy) == shape.contains(tx, ty)) |
|
214 None |
|
215 else { |
|
216 val (dx, dy) = (fx - tx, fy - ty) |
|
217 if ((dx * dx + dy * dy) < 1.0) { |
|
218 val at = AffineTransform.getTranslateInstance(fx, fy) |
|
219 at.rotate(- (math.atan2(dx, dy) + math.Pi / 2)) |
|
220 Some(at) |
|
221 } |
|
222 else { |
|
223 val (mx, my) = (fx + (tx - fx) / 2.0, fy + (ty - fy) / 2.0) |
|
224 if (shape.contains(fx, fy) == shape.contains(mx, my)) |
|
225 binary_search(((mx, my), (tx, ty)), shape) |
|
226 else |
|
227 binary_search(((fx, fy), (mx, my)), shape) |
|
228 } |
|
229 } |
|
230 } |
|
231 |
|
232 intersecting_line(path, shape) match { |
|
233 case None => None |
|
234 case Some(line) => binary_search(line, shape) |
|
235 } |
|
236 } |
|
237 |
|
238 def paint(g: Graphics2D, path: GeneralPath, shape: Shape) |
|
239 { |
|
240 position(path, shape) match { |
|
241 case None => |
|
242 case Some(at) => |
|
243 val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3) |
|
244 arrow.moveTo(0, 0) |
|
245 arrow.lineTo(-10, 4) |
|
246 arrow.lineTo(-6, 0) |
|
247 arrow.lineTo(-10, -4) |
|
248 arrow.lineTo(0, 0) |
|
249 arrow.transform(at) |
|
250 |
|
251 g.fill(arrow) |
|
252 } |
|
253 } |
|
254 } |
|
255 } |
|