src/Tools/Graphview/graphview.scala

--- a/src/Tools/Graphview/graphview.scala	Mon Sep 14 18:03:43 2015 +0200
+++ b/src/Tools/Graphview/graphview.scala	Mon Sep 14 19:46:50 2015 +0200
@@ -94,8 +94,8 @@
 
   def foreground_color: Color = Color.BLACK
   def background_color: Color = Color.WHITE
-  def selection_color: Color = Color.GREEN
-  def highlight_color: Color = Color.YELLOW
+  def selection_color: Color = new Color(204, 204, 255)
+  def highlight_color: Color = new Color(255, 255, 224)
   def error_color: Color = Color.RED
   def dummy_color: Color = Color.GRAY
 
@@ -116,6 +116,7 @@
   var show_content = false
   var show_arrow_heads = false
   var show_dummies = false
+  var editor_style = false
 
   object Colors
   {