Browse Source

GUI: In property editor dialog, place initial focus on the property text field

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11108 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 10 years ago
parent
commit
9ea440f147
  1. 6
      prism/src/userinterface/properties/GUIPropertyEditor.java

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

@ -114,6 +114,12 @@ public class GUIPropertyEditor extends javax.swing.JDialog implements ActionList
super.show();
// Request that the initial focus is placed on the property text field
// when the dialog is shown.
// This is not guaranteed to work, but if it does then it's
// convenient for the user...
if (propertyText != null) // should exist, but be careful nonetheless
propertyText.requestFocusInWindow();
}
public void dispose()

Loading…
Cancel
Save