diff --git a/prism/src/userinterface/GUIClipboard.java b/prism/src/userinterface/GUIClipboard.java index bc64c120..45b2a0ae 100644 --- a/prism/src/userinterface/GUIClipboard.java +++ b/prism/src/userinterface/GUIClipboard.java @@ -348,11 +348,6 @@ public class GUIClipboard extends GUIPlugin actionSelectAll.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallSelectAll.png")); } - public OptionsPanel getOptions() - { - return null; - } - public void notifySettings(prism.PrismSettings settings) {} diff --git a/prism/src/userinterface/GUIFileMenu.java b/prism/src/userinterface/GUIFileMenu.java index c9726a91..0655379a 100644 --- a/prism/src/userinterface/GUIFileMenu.java +++ b/prism/src/userinterface/GUIFileMenu.java @@ -62,11 +62,6 @@ public class GUIFileMenu extends GUIPlugin return menu; } - public OptionsPanel getOptions() - { - return null; - } - public String getTabText() { return ""; diff --git a/prism/src/userinterface/GUIGeneralOptions.form b/prism/src/userinterface/GUIGeneralOptions.form deleted file mode 100644 index 861ce6ef..00000000 --- a/prism/src/userinterface/GUIGeneralOptions.form +++ /dev/null @@ -1,69 +0,0 @@ - - -
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/prism/src/userinterface/GUIGeneralOptions.java b/prism/src/userinterface/GUIGeneralOptions.java deleted file mode 100644 index aa4e0dc3..00000000 --- a/prism/src/userinterface/GUIGeneralOptions.java +++ /dev/null @@ -1,183 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Andrew Hinton (University of Birmingham) -// * Dave Parker (University of Oxford, formerly University of Birmingham) -// -//------------------------------------------------------------------------------ -// -// This file is part of PRISM. -// -// PRISM is free software; you can redistribute it and/or modify -// it under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// PRISM is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU General Public License for more details. -// -// You should have received a copy of the GNU General Public License -// along with PRISM; if not, write to the Free Software Foundation, -// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -// -//============================================================================== - -package userinterface; - -import javax.swing.plaf.metal.*; -import javax.swing.*; -import userinterface.util.*; -import org.w3c.dom.DOMException; -import org.w3c.dom.Document; -import org.w3c.dom.Element; - -import userinterface.OptionsPanel; - -public class GUIGeneralOptions extends OptionsPanel -{ - private GUIPrism gui; - private int last; - private int adjust; - /** Creates new form GUIGeneralOptions */ - public GUIGeneralOptions(GUIPrism gui) - { - super("General"); - initComponents(); - this.gui = gui; - } - - /** This method is called from within the constructor to - * initialize the form. - * WARNING: Do NOT modify this code. The content of this method is - * always regenerated by the Form Editor. - */ - private void initComponents()//GEN-BEGIN:initComponents - { - java.awt.GridBagConstraints gridBagConstraints; - - jPanel1 = new javax.swing.JPanel(); - jPanel2 = new javax.swing.JPanel(); - jPanel3 = new javax.swing.JPanel(); - jLabel1 = new javax.swing.JLabel(); - adjustSlider = new javax.swing.JSlider(); - - setLayout(new java.awt.GridBagLayout()); - - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.gridx = 0; - gridBagConstraints.gridy = 2; - add(jPanel1, gridBagConstraints); - - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.gridx = 2; - gridBagConstraints.gridy = 0; - add(jPanel2, gridBagConstraints); - - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.gridx = 0; - gridBagConstraints.gridy = 0; - add(jPanel3, gridBagConstraints); - - jLabel1.setLabelFor(adjustSlider); - jLabel1.setText("User interface size:"); - gridBagConstraints = new java.awt.GridBagConstraints(); - gridBagConstraints.gridx = 1; - gridBagConstraints.gridy = 1; - gridBagConstraints.anchor = java.awt.GridBagConstraints.WEST; - add(jLabel1, gridBagConstraints); - - adjustSlider.setMajorTickSpacing(5); - adjustSlider.setMaximum(5); - adjustSlider.setMinimum(-5); - adjustSlider.setMinorTickSpacing(1); - adjustSlider.setPaintLabels(true); - adjustSlider.setPaintTicks(true); - adjustSlider.setSnapToTicks(true); - adjustSlider.setValue(0); - add(adjustSlider, new java.awt.GridBagConstraints()); - - }//GEN-END:initComponents - - public void apply() - { - - int adjust = 0; - - adjust = adjustSlider.getValue(); - if(adjust != last) - { - //System.out.println("adjustment = "+adjust); - try - { - MetalTheme theme = new PresentationMetalTheme(adjust); - MetalLookAndFeel.setCurrentTheme(theme); - UIManager.setLookAndFeel(UIManager.getLookAndFeel()); - } - catch(Exception e) - { - //System.out.println("Exception"); - return; - } - - SwingUtilities.updateComponentTreeUI(gui); - SwingUtilities.updateComponentTreeUI(gui.getOptions()); - - gui.pack(); - gui.getOptions().pack(); - gui.addNotify(); - last = adjust; - } - } - - public void synchronizeGUI() - { - //not needed - adjust = adjustSlider.getValue(); - last = adjust; - } - - public void defaultGUI() - { - adjustSlider.setValue(0); - - } - - public boolean valid() throws GUIException - { - return true; - } - - public Element saveXMLElement(Document doc) throws DOMException - { - return doc.createElement("dummy"); - } - - public void loadXMLElement(Element element) - { - } - - public void loadProperties(java.util.Properties properties) - { - } - - public void loadXMLElement(Document doc, Element element) - { - } - - public void saveProperties(java.util.Properties properties) - { - } - - // Variables declaration - do not modify//GEN-BEGIN:variables - javax.swing.JSlider adjustSlider; - private javax.swing.JLabel jLabel1; - private javax.swing.JPanel jPanel1; - private javax.swing.JPanel jPanel2; - private javax.swing.JPanel jPanel3; - // End of variables declaration//GEN-END:variables - - -} diff --git a/prism/src/userinterface/GUIOptionsDialog.java b/prism/src/userinterface/GUIOptionsDialog.java index b70648d1..a49bdc76 100644 --- a/prism/src/userinterface/GUIOptionsDialog.java +++ b/prism/src/userinterface/GUIOptionsDialog.java @@ -62,11 +62,6 @@ public class GUIOptionsDialog extends javax.swing.JDialog } } - public void addPanel(OptionsPanel p) - { - // defunct - } - public void show() { super.show(); diff --git a/prism/src/userinterface/GUIPlugin.java b/prism/src/userinterface/GUIPlugin.java index a083baba..c90bb06a 100644 --- a/prism/src/userinterface/GUIPlugin.java +++ b/prism/src/userinterface/GUIPlugin.java @@ -150,12 +150,6 @@ public abstract class GUIPlugin extends JPanel implements GUIEventListener, Pris */ public abstract JToolBar getToolBar(); - /** Abstract access method to be implemented to provide an OptionsPanel to be - * displayed as part of the OptionsDialog stored in the parent GUI. - * @return An OptionsPanel for this plugin. Returns null if no options panel is required. - */ - public abstract OptionsPanel getOptions(); - /** Returns an XML representation of this plugin, for use in saving the state of the * system to a file * @return The XML description diff --git a/prism/src/userinterface/GUIPrism.java b/prism/src/userinterface/GUIPrism.java index dade735d..c50b270a 100644 --- a/prism/src/userinterface/GUIPrism.java +++ b/prism/src/userinterface/GUIPrism.java @@ -308,9 +308,6 @@ public class GUIPrism extends JFrame if (plug.getToolBar() != null) { toolPanel.add(plug.getToolBar()); } - if (plug.getOptions() != null) { - options.addPanel(plug.getOptions()); - } if (plug instanceof userinterface.log.GUILog) { logPlug = (userinterface.log.GUILog) plug; } diff --git a/prism/src/userinterface/OptionsPanel.java b/prism/src/userinterface/OptionsPanel.java deleted file mode 100644 index 4c394252..00000000 --- a/prism/src/userinterface/OptionsPanel.java +++ /dev/null @@ -1,71 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Andrew Hinton (University of Birmingham) -// * Dave Parker (University of Oxford, formerly University of Birmingham) -// -//------------------------------------------------------------------------------ -// -// This file is part of PRISM. -// -// PRISM is free software; you can redistribute it and/or modify -// it under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// PRISM is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU General Public License for more details. -// -// You should have received a copy of the GNU General Public License -// along with PRISM; if not, write to the Free Software Foundation, -// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -// -//============================================================================== - -package userinterface; - -import javax.swing.*; -import prism.*; - -public abstract class OptionsPanel extends JPanel -{ - - private String tab; - - public OptionsPanel(String tab) - { - this.tab = tab; - } - - //Applies the state of the options panel to the data stored in PrismSettings - public abstract void apply() throws PrismException; - - //Sets up the gui to reflect the data stored in - public abstract void synchronizeGUI(); - - //The following methods are now irrelevent: - // All loading/saving is now done in PrismSettings.java - // Default settings are handled in PrismSettings.java - // and validity is now handled in the apply() method - - //public abstract void defaultGUI(); - - //public abstract boolean valid() throws GUIException; - - //public abstract Element saveXMLElement(Document doc) throws DOMException; - - //public abstract void loadXMLElement(Document doc, Element element); - - //public abstract void saveProperties(Properties properties); - - //public abstract void loadProperties(Properties properties); - - public String getTabText() - { - return tab; - } - -} diff --git a/prism/src/userinterface/log/GUILog.java b/prism/src/userinterface/log/GUILog.java index 9e4121fe..f9d29807 100644 --- a/prism/src/userinterface/log/GUILog.java +++ b/prism/src/userinterface/log/GUILog.java @@ -56,7 +56,6 @@ import prism.PrismSettingsListener; import userinterface.GUIClipboardEvent; import userinterface.GUIPlugin; import userinterface.GUIPrism; -import userinterface.OptionsPanel; import userinterface.util.GUIEvent; import userinterface.util.GUILogEvent; @@ -302,11 +301,6 @@ public class GUILog extends GUIPlugin implements MouseListener, PrismSettingsLis } } - public OptionsPanel getOptions() - { - return null; - } - public void notifySettings(PrismSettings settings) { if(theLog instanceof GUIWindowLog) diff --git a/prism/src/userinterface/model/GUIMultiModel.java b/prism/src/userinterface/model/GUIMultiModel.java index 4c0712e5..98428c66 100644 --- a/prism/src/userinterface/model/GUIMultiModel.java +++ b/prism/src/userinterface/model/GUIMultiModel.java @@ -60,7 +60,6 @@ import prism.PrismSettingsListener; import userinterface.GUIClipboardEvent; import userinterface.GUIPlugin; import userinterface.GUIPrism; -import userinterface.OptionsPanel; import userinterface.util.GUIComputationEvent; import userinterface.util.GUIEvent; import userinterface.util.GUIExitEvent; @@ -1204,11 +1203,6 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener doEnables(); } - public OptionsPanel getOptions() - { - return null; - } - public void notifySettings(PrismSettings settings) { //System.out.println("model notifySettings called"); diff --git a/prism/src/userinterface/model/GUITextModelEditorGutter.java b/prism/src/userinterface/model/GUITextModelEditorGutter.java index 1a5e76e8..a45c5daf 100644 --- a/prism/src/userinterface/model/GUITextModelEditorGutter.java +++ b/prism/src/userinterface/model/GUITextModelEditorGutter.java @@ -50,7 +50,6 @@ import javax.swing.text.JTextComponent; import prism.PrismSettings; import userinterface.GUIPrism; -import userinterface.OptionsPanel; /** * Information gutter for the text model editor. It displays line numbers for @@ -365,7 +364,6 @@ public class GUITextModelEditorGutter extends JPanel implements PropertyChangeLi public boolean displaysTab() {return false;} public JMenu getMenu() {return null;} - public OptionsPanel getOptions() {return null;} public String getTabText() {return null;} public JToolBar getToolBar() {return null;} public String getXMLIDTag() {return null;} diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index db664ab0..78d41bdf 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -104,7 +104,6 @@ import userinterface.GUIConstantsPicker; import userinterface.GUIPlugin; import userinterface.GUIPrism; import userinterface.GUISimulationPicker; -import userinterface.OptionsPanel; import userinterface.SimulationInformation; import userinterface.graph.Graph; import userinterface.graph.Graph.SeriesKey; @@ -1249,11 +1248,6 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List return propMenu; } - public OptionsPanel getOptions() - { - return null; - } - public String getTabText() { return "Properties"; diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 9ff754ce..45714e7f 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -75,7 +75,6 @@ import simulator.SimulatorEngine; import userinterface.GUIConstantsPicker; import userinterface.GUIPlugin; import userinterface.GUIPrism; -import userinterface.OptionsPanel; import userinterface.graph.Graph; import userinterface.model.GUIModelEvent; import userinterface.model.GUIMultiModel; @@ -946,11 +945,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect return simulatorMenu; } - public OptionsPanel getOptions() - { - return null; - } - public String getTabText() { return "Simulator";