back to more basic defaults, independently on the accidental L&F: e.g. relevant for editor_style=false, and session_graph.pdf;
authorwenzelm
Tue, 22 Jul 2025 12:02:53 +0200
changeset 82894 a8e47bd31965
parent 82893 d6a14ed060fb
child 82895 83b9639f5c42
back to more basic defaults, independently on the accidental L&F: e.g. relevant for editor_style=false, and session_graph.pdf;
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 */