equal
deleted
inserted
replaced
22 object Node |
22 object Node |
23 { |
23 { |
24 def shape(visualizer: Visualizer, node: Graph_Display.Node): Rectangle2D.Double = |
24 def shape(visualizer: Visualizer, node: Graph_Display.Node): Rectangle2D.Double = |
25 { |
25 { |
26 val metrics = visualizer.metrics |
26 val metrics = visualizer.metrics |
27 val p = visualizer.Coordinates.get_node(node) |
27 val p = visualizer.get_vertex(Layout.Node(node)) |
28 val bounds = metrics.string_bounds(node.toString) |
28 val bounds = metrics.string_bounds(node.toString) |
29 val w = bounds.getWidth + metrics.pad_x |
29 val w2 = ((bounds.getWidth + metrics.pad_x) / 2).ceil |
30 val h = bounds.getHeight + metrics.pad_y |
30 val h2 = ((bounds.getHeight + metrics.pad_y) / 2).ceil |
31 new Rectangle2D.Double((p.x - (w / 2)).floor, (p.y - (h / 2)).floor, w.ceil, h.ceil) |
31 new Rectangle2D.Double(p.x - w2, p.y - h2, 2 * w2, 2 * h2) |
32 } |
32 } |
33 |
33 |
34 def paint(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node) |
34 def paint(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node) |
35 { |
35 { |
36 val metrics = visualizer.metrics |
36 val metrics = visualizer.metrics |
56 object Dummy |
56 object Dummy |
57 { |
57 { |
58 def shape(visualizer: Visualizer, d: Layout.Point): Rectangle2D.Double = |
58 def shape(visualizer: Visualizer, d: Layout.Point): Rectangle2D.Double = |
59 { |
59 { |
60 val metrics = visualizer.metrics |
60 val metrics = visualizer.metrics |
61 val w = metrics.pad_x |
61 val w = metrics.dummy_width2 |
62 new Rectangle2D.Double((d.x - (w / 2)).floor, (d.y - (w / 2)).floor, w.ceil, w.ceil) |
62 new Rectangle2D.Double(d.x - w / 2, d.y - w / 2, w, w) |
63 } |
63 } |
64 |
64 |
65 def paint(gfx: Graphics2D, visualizer: Visualizer, d: Layout.Point) |
65 def paint(gfx: Graphics2D, visualizer: Visualizer, d: Layout.Point) |
66 { |
66 { |
67 gfx.setStroke(default_stroke) |
67 gfx.setStroke(default_stroke) |
72 |
72 |
73 object Straight_Edge |
73 object Straight_Edge |
74 { |
74 { |
75 def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge) |
75 def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge) |
76 { |
76 { |
77 val p = visualizer.Coordinates.get_node(edge._1) |
77 val p = visualizer.get_vertex(Layout.Node(edge._1)) |
78 val q = visualizer.Coordinates.get_node(edge._2) |
78 val q = visualizer.get_vertex(Layout.Node(edge._2)) |
79 val ds = |
79 val ds = |
80 { |
80 { |
81 val a = p.y min q.y |
81 val a = p.y min q.y |
82 val b = p.y max q.y |
82 val b = p.y max q.y |
83 visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b) |
83 visualizer.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList |
84 } |
84 } |
85 val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) |
85 val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) |
86 |
86 |
87 path.moveTo(p.x, p.y) |
87 path.moveTo(p.x, p.y) |
88 ds.foreach(d => path.lineTo(d.x, d.y)) |
88 ds.foreach(d => path.lineTo(d.x, d.y)) |
104 { |
104 { |
105 private val slack = 0.1 |
105 private val slack = 0.1 |
106 |
106 |
107 def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge) |
107 def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge) |
108 { |
108 { |
109 val p = visualizer.Coordinates.get_node(edge._1) |
109 val p = visualizer.get_vertex(Layout.Node(edge._1)) |
110 val q = visualizer.Coordinates.get_node(edge._2) |
110 val q = visualizer.get_vertex(Layout.Node(edge._2)) |
111 val ds = |
111 val ds = |
112 { |
112 { |
113 val a = p.y min q.y |
113 val a = p.y min q.y |
114 val b = p.y max q.y |
114 val b = p.y max q.y |
115 visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b) |
115 visualizer.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList |
116 } |
116 } |
117 |
117 |
118 if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge) |
118 if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge) |
119 else { |
119 else { |
120 val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) |
120 val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) |