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