Browse Source

Graph chooser dialog defaults to last graph created for "existing graph".

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5413 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
commit
f412d3115e
  1. 6
      prism/src/userinterface/properties/GUIGraphPicker.java

6
prism/src/userinterface/properties/GUIGraphPicker.java

@ -269,8 +269,12 @@ public class GUIGraphPicker extends javax.swing.JDialog
for (int i = 0; i < graphHandler.getNumModels(); i++) { for (int i = 0; i < graphHandler.getNumModels(); i++) {
existingGraphCombo.addItem(graphHandler.getGraphName(i)); existingGraphCombo.addItem(graphHandler.getGraphName(i));
} }
// default to latest one
if (existingGraphCombo.getItemCount() > 0) {
existingGraphCombo.setSelectedIndex(existingGraphCombo.getItemCount() - 1);
}
// if there are no graphs, disable control // if there are no graphs, disable control
if (graphHandler.getNumModels() == 0) {
else {
existingGraphCombo.setEnabled(false); existingGraphCombo.setEnabled(false);
this.existingGraphRadio.setEnabled(false); this.existingGraphRadio.setEnabled(false);
} }

Loading…
Cancel
Save