From f412d3115ebeb3c9bfee6f1dcdcbac2fe0d33d7a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 2 Jul 2012 09:22:52 +0000 Subject: [PATCH] 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 --- prism/src/userinterface/properties/GUIGraphPicker.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/prism/src/userinterface/properties/GUIGraphPicker.java b/prism/src/userinterface/properties/GUIGraphPicker.java index dc8ba5af..c7a27e6f 100644 --- a/prism/src/userinterface/properties/GUIGraphPicker.java +++ b/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++) { 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 (graphHandler.getNumModels() == 0) { + else { existingGraphCombo.setEnabled(false); this.existingGraphRadio.setEnabled(false); }