--- a/src/Tools/Graphview/graph_panel.scala Mon Jan 05 23:05:17 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Mon Jan 05 23:29:38 2015 +0100
@@ -96,7 +96,7 @@
gfx.fillRect(0, 0, peer.getWidth, peer.getHeight)
gfx.transform(Transform())
- visualizer.Drawer.paint_all_visible(gfx, true)
+ visualizer.paint_all_visible(gfx)
}
}
private val paint_panel = new Paint_Panel
--- a/src/Tools/Graphview/main_panel.scala Mon Jan 05 23:05:17 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala Mon Jan 05 23:29:38 2015 +0100
@@ -43,6 +43,10 @@
selected = visualizer.arrow_heads
action = Action("Arrow heads") { visualizer.arrow_heads = selected; graph_panel.repaint() }
},
+ new CheckBox() {
+ selected = visualizer.show_dummies
+ action = Action("Show dummies") { visualizer.show_dummies = selected; graph_panel.repaint() }
+ },
new Button {
action = Action("Save image") {
chooser.showSaveDialog(this) match {
@@ -71,7 +75,7 @@
gfx.setColor(Color.WHITE)
gfx.fillRect(0, 0, w, h)
gfx.translate(- box.x, - box.y)
- visualizer.Drawer.paint_all_visible(gfx, false)
+ visualizer.paint_all_visible(gfx)
}
try {
--- a/src/Tools/Graphview/shapes.scala Mon Jan 05 23:05:17 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala Mon Jan 05 23:29:38 2015 +0100
@@ -72,8 +72,7 @@
object Straight_Edge
{
- def paint(gfx: Graphics2D, visualizer: Visualizer,
- edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
+ def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
{
val p = visualizer.Coordinates.get_node(edge._1)
val q = visualizer.Coordinates.get_node(edge._2)
@@ -89,13 +88,15 @@
ds.foreach(d => path.lineTo(d.x, d.y))
path.lineTo(q.x, q.y)
- if (dummies) ds.foreach(Dummy.paint(gfx, visualizer, _))
+ if (visualizer.show_dummies)
+ ds.foreach(Dummy.paint(gfx, visualizer, _))
gfx.setStroke(default_stroke)
gfx.setColor(visualizer.edge_color(edge))
gfx.draw(path)
- if (head) Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
+ if (visualizer.arrow_heads)
+ Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
}
}
@@ -103,8 +104,7 @@
{
private val slack = 0.1
- def paint(gfx: Graphics2D, visualizer: Visualizer,
- edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
+ def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
{
val p = visualizer.Coordinates.get_node(edge._1)
val q = visualizer.Coordinates.get_node(edge._2)
@@ -115,7 +115,7 @@
visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b)
}
- if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge, head, dummies)
+ if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge)
else {
val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
path.moveTo(p.x, p.y)
@@ -142,13 +142,15 @@
q.x - slack * dx2, q.y - slack * dy2,
q.x, q.y)
- if (dummies) ds.foreach(Dummy.paint(gfx, visualizer, _))
+ if (visualizer.show_dummies)
+ ds.foreach(Dummy.paint(gfx, visualizer, _))
gfx.setStroke(default_stroke)
gfx.setColor(visualizer.edge_color(edge))
gfx.draw(path)
- if (head) Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
+ if (visualizer.arrow_heads)
+ Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
}
}
}
--- 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