src/Tools/Graphview/graphview.scala
changeset 82894 a8e47bd31965
parent 82626 e840461d5370
--- a/src/Tools/Graphview/graphview.scala	Tue Jul 22 11:55:42 2025 +0200
+++ b/src/Tools/Graphview/graphview.scala	Tue Jul 22 12:02:53 2025 +0200
@@ -90,12 +90,12 @@
 
   /* main colors */
 
-  def foreground_color: Color = GUI.default_foreground_color()
-  def background_color: Color = GUI.default_background_color()
+  def foreground_color: Color = Color.BLACK
+  def background_color: Color = Color.WHITE
   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 = GUI.default_intermediate_color()
+  def dummy_color: Color = Color.GRAY
 
 
   /* font rendering information */