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.get_vertex(Layout.Node(node)) |
27 val p = visualizer.layout.get_vertex(Layout.Node(node)) |
28 val bounds = metrics.string_bounds(node.toString) |
28 val bounds = metrics.string_bounds(node.toString) |
29 val w2 = ((bounds.getWidth + metrics.pad_x) / 2).ceil |
29 val w2 = ((bounds.getWidth + metrics.pad_x) / 2).ceil |
30 val h2 = ((bounds.getHeight + metrics.pad_y) / 2).ceil |
30 val h2 = ((bounds.getHeight + metrics.pad_y) / 2).ceil |
31 new Rectangle2D.Double(p.x - w2, p.y - h2, 2 * w2, 2 * h2) |
31 new Rectangle2D.Double(p.x - w2, p.y - h2, 2 * w2, 2 * h2) |
32 } |
32 } |
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.get_vertex(Layout.Node(edge._1)) |
77 val p = visualizer.layout.get_vertex(Layout.Node(edge._1)) |
78 val q = visualizer.get_vertex(Layout.Node(edge._2)) |
78 val q = visualizer.layout.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.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList |
83 visualizer.layout.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.get_vertex(Layout.Node(edge._1)) |
109 val p = visualizer.layout.get_vertex(Layout.Node(edge._1)) |
110 val q = visualizer.get_vertex(Layout.Node(edge._2)) |
110 val q = visualizer.layout.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.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList |
115 visualizer.layout.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) |