# HG changeset patch
# User wenzelm
# Date 1421681881 -3600
# Node ID d43434c60d3a2d2a41e3ff2a0cfe9622e32668f5
# Parent  283aa6225d987a2b285b34cd1ec6957cf1d13e6b
clarified edge_color;

diff -r 283aa6225d98 -r d43434c60d3a src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Mon Jan 19 16:31:04 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Mon Jan 19 16:38:01 2015 +0100
@@ -76,7 +76,7 @@
       if (visualizer.show_dummies) ds.foreach(paint_dummy(gfx, visualizer, _))
 
       gfx.setStroke(default_stroke)
-      gfx.setColor(visualizer.edge_color(edge))
+      gfx.setColor(visualizer.edge_color(edge, p.y < q.y))
       gfx.draw(path)
 
       if (visualizer.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q))
@@ -128,7 +128,7 @@
         if (visualizer.show_dummies) ds.foreach(paint_dummy(gfx, visualizer, _))
 
         gfx.setStroke(default_stroke)
-        gfx.setColor(visualizer.edge_color(edge))
+        gfx.setColor(visualizer.edge_color(edge, p.y < q.y))
         gfx.draw(path)
 
         if (visualizer.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q))
diff -r 283aa6225d98 -r d43434c60d3a src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Mon Jan 19 16:31:04 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Mon Jan 19 16:38:01 2015 +0100
@@ -168,5 +168,7 @@
     else
       Node_Color(foreground_color, model.colors.getOrElse(node, background_color), foreground_color)
 
-  def edge_color(edge: Graph_Display.Edge): Color = foreground_color
+  def edge_color(edge: Graph_Display.Edge, downwards: Boolean): Color =
+    if (downwards || show_arrow_heads) foreground_color
+    else error_color
 }
\ No newline at end of file