author | wenzelm |
Sun, 04 Jan 2015 13:34:42 +0100 | |
changeset 59258 | d5c9900636ef |
parent 59251 | b12d76aa29fb |
child 59262 | 5cd92c743958 |
permissions | -rw-r--r-- |
59202 | 1 |
/* Title: Tools/Graphview/shapes.scala |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Markus Kaiser, TU Muenchen |
59240 | 3 |
Author: Makarius |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
4 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
5 |
Drawable shapes. |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
6 |
*/ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
7 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
8 |
package isabelle.graphview |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
9 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
10 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
11 |
import isabelle._ |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
12 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
13 |
import java.awt.{BasicStroke, Graphics2D, Shape} |
50467 | 14 |
import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, PathIterator} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
15 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
16 |
|
50467 | 17 |
object Shapes |
18 |
{ |
|
59249 | 19 |
private val default_stroke = |
20 |
new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) |
|
21 |
||
59258 | 22 |
object Node |
50467 | 23 |
{ |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
24 |
def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node) |
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
25 |
: Rectangle2D.Double = |
50467 | 26 |
{ |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
27 |
val (x, y) = visualizer.Coordinates(node) |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
28 |
val bounds = m.string_bounds(node.toString) |
59236 | 29 |
val w = bounds.getWidth + m.pad |
30 |
val h = bounds.getHeight + m.pad |
|
59242 | 31 |
new Rectangle2D.Double((x - (w / 2)).floor, (y - (h / 2)).floor, w.ceil, h.ceil) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
32 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
33 |
|
59250 | 34 |
def paint(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node) |
50467 | 35 |
{ |
59250 | 36 |
val m = Visualizer.Metrics(gfx) |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
37 |
val s = shape(m, visualizer, node) |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
38 |
val c = visualizer.node_color(node) |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
39 |
val bounds = m.string_bounds(node.toString) |
59236 | 40 |
|
59250 | 41 |
gfx.setColor(c.background) |
42 |
gfx.fill(s) |
|
59242 | 43 |
|
59250 | 44 |
gfx.setColor(c.border) |
45 |
gfx.setStroke(default_stroke) |
|
46 |
gfx.draw(s) |
|
59242 | 47 |
|
59250 | 48 |
gfx.setColor(c.foreground) |
49 |
gfx.drawString(node.toString, |
|
59242 | 50 |
(s.getCenterX - bounds.getWidth / 2).round.toInt, |
51 |
(s.getCenterY - bounds.getHeight / 2 + m.ascent).round.toInt) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
52 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
53 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
54 |
|
59248 | 55 |
object Dummy |
50467 | 56 |
{ |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
57 |
private val identity = new AffineTransform() |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
58 |
|
59251 | 59 |
def shape(m: Visualizer.Metrics, visualizer: Visualizer): Shape = |
59242 | 60 |
{ |
61 |
val w = (m.space_width / 2).ceil |
|
62 |
new Rectangle2D.Double(- w, - w, 2 * w, 2 * w) |
|
63 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
64 |
|
59251 | 65 |
def paint(gfx: Graphics2D, visualizer: Visualizer): Unit = |
66 |
paint_transformed(gfx, visualizer, identity) |
|
50467 | 67 |
|
59251 | 68 |
def paint_transformed(gfx: Graphics2D, visualizer: Visualizer, at: AffineTransform) |
50464 | 69 |
{ |
59250 | 70 |
val m = Visualizer.Metrics(gfx) |
59251 | 71 |
val s = shape(m, visualizer) |
59242 | 72 |
|
59250 | 73 |
gfx.setStroke(default_stroke) |
59251 | 74 |
gfx.setColor(visualizer.dummy_color) |
59250 | 75 |
gfx.draw(at.createTransformedShape(s)) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
76 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
77 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
78 |
|
59248 | 79 |
object Straight_Edge |
50467 | 80 |
{ |
59250 | 81 |
def paint(gfx: Graphics2D, visualizer: Visualizer, |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
82 |
edge: Graph_Display.Edge, head: Boolean, dummies: Boolean) |
50464 | 83 |
{ |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
84 |
val (fx, fy) = visualizer.Coordinates(edge._1) |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
85 |
val (tx, ty) = visualizer.Coordinates(edge._2) |
50468 | 86 |
val ds = |
87 |
{ |
|
88 |
val min = fy min ty |
|
89 |
val max = fy max ty |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
90 |
visualizer.Coordinates(edge).filter({ case (_, y) => min < y && y < max }) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
91 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
92 |
val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
93 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
94 |
path.moveTo(fx, fy) |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
95 |
ds.foreach({ case (x, y) => path.lineTo(x, y) }) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
96 |
path.lineTo(tx, ty) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
97 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
98 |
if (dummies) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
99 |
ds.foreach({ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
100 |
case (x, y) => { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
101 |
val at = AffineTransform.getTranslateInstance(x, y) |
59251 | 102 |
Dummy.paint_transformed(gfx, visualizer, at) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
103 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
104 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
105 |
} |
50467 | 106 |
|
59250 | 107 |
gfx.setStroke(default_stroke) |
108 |
gfx.setColor(visualizer.edge_color(edge)) |
|
109 |
gfx.draw(path) |
|
50467 | 110 |
|
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
111 |
if (head) |
59250 | 112 |
Arrow_Head.paint(gfx, path, |
113 |
visualizer.Drawer.shape(Visualizer.Metrics(gfx), edge._2)) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
114 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
115 |
} |
50467 | 116 |
|
59248 | 117 |
object Cardinal_Spline_Edge |
50467 | 118 |
{ |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
119 |
private val slack = 0.1 |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
120 |
|
59250 | 121 |
def paint(gfx: Graphics2D, visualizer: Visualizer, |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
122 |
edge: Graph_Display.Edge, head: Boolean, dummies: Boolean) |
50464 | 123 |
{ |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
124 |
val (fx, fy) = visualizer.Coordinates(edge._1) |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
125 |
val (tx, ty) = visualizer.Coordinates(edge._2) |
50468 | 126 |
val ds = |
127 |
{ |
|
128 |
val min = fy min ty |
|
129 |
val max = fy max ty |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
130 |
visualizer.Coordinates(edge).filter({ case (_, y) => min < y && y < max }) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
131 |
} |
50467 | 132 |
|
59250 | 133 |
if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge, head, dummies) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
134 |
else { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
135 |
val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
136 |
path.moveTo(fx, fy) |
50467 | 137 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
138 |
val coords = ((fx, fy) :: ds ::: List((tx, ty))) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
139 |
val (dx, dy) = (coords(2)._1 - coords(0)._1, coords(2)._2 - coords(0)._2) |
50467 | 140 |
|
141 |
val (dx2, dy2) = |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
142 |
((dx, dy) /: coords.sliding(3))({ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
143 |
case ((dx, dy), List((lx, ly), (mx, my), (rx, ry))) => { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
144 |
val (dx2, dy2) = (rx - lx, ry - ly) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
145 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
146 |
path.curveTo(lx + slack * dx , ly + slack * dy, |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
147 |
mx - slack * dx2, my - slack * dy2, |
50467 | 148 |
mx , my) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
149 |
(dx2, dy2) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
150 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
151 |
}) |
50467 | 152 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
153 |
val (lx, ly) = ds.last |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
154 |
path.curveTo(lx + slack * dx2, ly + slack * dy2, |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
155 |
tx - slack * dx2, ty - slack * dy2, |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
156 |
tx , ty) |
50467 | 157 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
158 |
if (dummies) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
159 |
ds.foreach({ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
160 |
case (x, y) => { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
161 |
val at = AffineTransform.getTranslateInstance(x, y) |
59251 | 162 |
Dummy.paint_transformed(gfx, visualizer, at) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
163 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
164 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
165 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
166 |
|
59250 | 167 |
gfx.setStroke(default_stroke) |
168 |
gfx.setColor(visualizer.edge_color(edge)) |
|
169 |
gfx.draw(path) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
170 |
|
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
171 |
if (head) |
59250 | 172 |
Arrow_Head.paint(gfx, path, |
173 |
visualizer.Drawer.shape(Visualizer.Metrics(gfx), edge._2)) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
174 |
} |
50467 | 175 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
176 |
} |
50467 | 177 |
|
178 |
object Arrow_Head |
|
179 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
180 |
type Point = (Double, Double) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
181 |
|
50467 | 182 |
private def position(path: GeneralPath, shape: Shape): Option[AffineTransform] = |
183 |
{ |
|
184 |
def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] = |
|
185 |
{ |
|
49745 | 186 |
val i = path.getPathIterator(null, 1.0) |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
187 |
val seg = Array[Double](0.0, 0.0, 0.0, 0.0, 0.0, 0.0) |
49745 | 188 |
var p1 = (0.0, 0.0) |
189 |
var p2 = (0.0, 0.0) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
190 |
while (!i.isDone()) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
191 |
i.currentSegment(seg) match { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
192 |
case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1)) |
50467 | 193 |
case PathIterator.SEG_LINETO => |
194 |
p1 = p2 |
|
195 |
p2 = (seg(0), seg(1)) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
196 |
|
50467 | 197 |
if(shape.contains(seg(0), seg(1))) |
198 |
return Some((p1, p2)) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
199 |
case _ => |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
200 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
201 |
i.next() |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
202 |
} |
50467 | 203 |
None |
204 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
205 |
|
50467 | 206 |
def binary_search(line: (Point, Point), shape: Shape): Option[AffineTransform] = |
207 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
208 |
val ((fx, fy), (tx, ty)) = line |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
209 |
if (shape.contains(fx, fy) == shape.contains(tx, ty)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
210 |
None |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
211 |
else { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
212 |
val (dx, dy) = (fx - tx, fy - ty) |
49745 | 213 |
if ((dx * dx + dy * dy) < 1.0) { |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
214 |
val at = AffineTransform.getTranslateInstance(fx, fy) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
215 |
at.rotate(- (math.atan2(dx, dy) + math.Pi / 2)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
216 |
Some(at) |
50467 | 217 |
} |
218 |
else { |
|
49745 | 219 |
val (mx, my) = (fx + (tx - fx) / 2.0, fy + (ty - fy) / 2.0) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
220 |
if (shape.contains(fx, fy) == shape.contains(mx, my)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
221 |
binary_search(((mx, my), (tx, ty)), shape) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
222 |
else |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
223 |
binary_search(((fx, fy), (mx, my)), shape) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
224 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
225 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
226 |
} |
50467 | 227 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
228 |
intersecting_line(path, shape) match { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
229 |
case None => None |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
230 |
case Some(line) => binary_search(line, shape) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
231 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
232 |
} |
50467 | 233 |
|
59250 | 234 |
def paint(gfx: Graphics2D, path: GeneralPath, shape: Shape) |
50464 | 235 |
{ |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
236 |
position(path, shape) match { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
237 |
case None => |
50479 | 238 |
case Some(at) => |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
239 |
val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
240 |
arrow.moveTo(0, 0) |
50479 | 241 |
arrow.lineTo(-10, 4) |
242 |
arrow.lineTo(-6, 0) |
|
243 |
arrow.lineTo(-10, -4) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
244 |
arrow.lineTo(0, 0) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
245 |
arrow.transform(at) |
59250 | 246 |
gfx.fill(arrow) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
247 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
248 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
249 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
250 |
} |