--- a/src/Tools/Graphview/visualizer.scala Mon Jan 05 23:05:17 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala Mon Jan 05 23:29:38 2015 +0100
@@ -52,7 +52,9 @@
/* rendering parameters */
+ // owned by GUI thread
var arrow_heads = false
+ var show_dummies = false
object Colors
{
@@ -74,6 +76,14 @@
}
}
+ def paint_all_visible(gfx: Graphics2D)
+ {
+ gfx.setRenderingHints(Metrics.rendering_hints)
+ for (edge <- visible_graph.edges_iterator)
+ Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge)
+ for (node <- visible_graph.keys_iterator)
+ Shapes.Node.paint(gfx, visualizer, node)
+ }
object Coordinates
{
@@ -129,22 +139,6 @@
}
}
- object Drawer
- {
- def apply(gfx: Graphics2D, node: Graph_Display.Node): Unit =
- if (!node.is_dummy) Shapes.Node.paint(gfx, visualizer, node)
-
- def apply(gfx: Graphics2D, edge: Graph_Display.Edge, head: Boolean, dummies: Boolean): Unit =
- Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge, head, dummies)
-
- def paint_all_visible(gfx: Graphics2D, dummies: Boolean)
- {
- gfx.setRenderingHints(Metrics.rendering_hints)
- visible_graph.edges_iterator.foreach(apply(gfx, _, arrow_heads, dummies))
- visible_graph.keys_iterator.foreach(apply(gfx, _))
- }
- }
-
object Selection
{
// owned by GUI thread