From c977d2c688cd10feb1eb702de3b6be1f1e8a4901 Mon Sep 17 00:00:00 2001 From: Mark Kattenbelt Date: Wed, 10 Dec 2008 11:31:32 +0000 Subject: [PATCH] set graph background colour to white by default git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@887 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/graph/DisplaySettings.java | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/prism/src/userinterface/graph/DisplaySettings.java b/prism/src/userinterface/graph/DisplaySettings.java index aff0ac36..fb7643ce 100644 --- a/prism/src/userinterface/graph/DisplaySettings.java +++ b/prism/src/userinterface/graph/DisplaySettings.java @@ -39,7 +39,9 @@ import settings.SettingException; import settings.SettingOwner; import java.awt.*; - + +import javax.swing.UIManager; + /** * Representation of the display settings of a Graph. * The settings are propagated to the JFreeChart library. @@ -68,11 +70,12 @@ public class DisplaySettings extends Observable implements SettingOwner this.plot = chart.getXYPlot(); antiAlias = new BooleanSetting("anti-aliasing", new Boolean(true), "Should the graph be rendered using anti-aliasing?", this, false); + Color defaultColor = Color.white; - Color defaultColor = Color.white; - - if (chart.getBackgroundPaint() instanceof Color) - defaultColor = ((Color)chart.getBackgroundPaint()); + //Color defaultColor = UIManager.getColor("Panel.background"); + + //if (chart.getBackgroundPaint() instanceof Color) + // defaultColor = ((Color)chart.getBackgroundPaint()); backgroundColor = new ColorSetting("background colour", defaultColor, "The background colour of the graph panel", this, false);