# HG changeset patch # User wenzelm # Date 1420496978 -3600 # Node ID 126293918a37ba04f4495ae3a7e6ed02b98f51e2 # Parent 305e79989d48d3ae993f1afbdc96fec0c8e35259 clarified visualizer parameters; do not show dummies by default; diff -r 305e79989d48 -r 126293918a37 src/Tools/Graphview/graph_panel.scala --- 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 diff -r 305e79989d48 -r 126293918a37 src/Tools/Graphview/main_panel.scala --- 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 { diff -r 305e79989d48 -r 126293918a37 src/Tools/Graphview/shapes.scala --- 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)) } } } diff -r 305e79989d48 -r 126293918a37 src/Tools/Graphview/visualizer.scala --- 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