back to more basic defaults, independently on the accidental L&F: e.g. relevant for editor_style=false, and session_graph.pdf;
--- 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 */