Browse Source

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
master
Mark Kattenbelt 17 years ago
parent
commit
c977d2c688
  1. 13
      prism/src/userinterface/graph/DisplaySettings.java

13
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);

Loading…
Cancel
Save