diff -r d6a14ed060fb -r a8e47bd31965 src/Tools/Graphview/graphview.scala --- 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 */