equal
deleted
inserted
replaced
50 } |
50 } |
51 |
51 |
52 |
52 |
53 /* rendering parameters */ |
53 /* rendering parameters */ |
54 |
54 |
|
55 // owned by GUI thread |
55 var arrow_heads = false |
56 var arrow_heads = false |
|
57 var show_dummies = false |
56 |
58 |
57 object Colors |
59 object Colors |
58 { |
60 { |
59 private val filter_colors = List( |
61 private val filter_colors = List( |
60 new Color(0xD9, 0xF2, 0xE2), // blue |
62 new Color(0xD9, 0xF2, 0xE2), // blue |
72 curr = (curr + 1) % filter_colors.length |
74 curr = (curr + 1) % filter_colors.length |
73 filter_colors(curr) |
75 filter_colors(curr) |
74 } |
76 } |
75 } |
77 } |
76 |
78 |
|
79 def paint_all_visible(gfx: Graphics2D) |
|
80 { |
|
81 gfx.setRenderingHints(Metrics.rendering_hints) |
|
82 for (edge <- visible_graph.edges_iterator) |
|
83 Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge) |
|
84 for (node <- visible_graph.keys_iterator) |
|
85 Shapes.Node.paint(gfx, visualizer, node) |
|
86 } |
77 |
87 |
78 object Coordinates |
88 object Coordinates |
79 { |
89 { |
80 def get_node(node: Graph_Display.Node): Layout.Point = layout.get_node(node) |
90 def get_node(node: Graph_Display.Node): Layout.Point = layout.get_node(node) |
81 def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] = layout.get_dummies(edge) |
91 def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] = layout.get_dummies(edge) |
127 y1 = (y1 + gap).ceil |
137 y1 = (y1 + gap).ceil |
128 new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0) |
138 new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0) |
129 } |
139 } |
130 } |
140 } |
131 |
141 |
132 object Drawer |
|
133 { |
|
134 def apply(gfx: Graphics2D, node: Graph_Display.Node): Unit = |
|
135 if (!node.is_dummy) Shapes.Node.paint(gfx, visualizer, node) |
|
136 |
|
137 def apply(gfx: Graphics2D, edge: Graph_Display.Edge, head: Boolean, dummies: Boolean): Unit = |
|
138 Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge, head, dummies) |
|
139 |
|
140 def paint_all_visible(gfx: Graphics2D, dummies: Boolean) |
|
141 { |
|
142 gfx.setRenderingHints(Metrics.rendering_hints) |
|
143 visible_graph.edges_iterator.foreach(apply(gfx, _, arrow_heads, dummies)) |
|
144 visible_graph.keys_iterator.foreach(apply(gfx, _)) |
|
145 } |
|
146 } |
|
147 |
|
148 object Selection |
142 object Selection |
149 { |
143 { |
150 // owned by GUI thread |
144 // owned by GUI thread |
151 private var state: List[Graph_Display.Node] = Nil |
145 private var state: List[Graph_Display.Node] = Nil |
152 |
146 |