From 9ea440f1471c1832d60e00cc41d7e69193eaa8f7 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 5 Jan 2016 10:08:26 +0000 Subject: [PATCH] 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 --- prism/src/userinterface/properties/GUIPropertyEditor.java | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/prism/src/userinterface/properties/GUIPropertyEditor.java b/prism/src/userinterface/properties/GUIPropertyEditor.java index 42c7e467..6b1496d0 100644 --- a/prism/src/userinterface/properties/GUIPropertyEditor.java +++ b/prism/src/userinterface/properties/GUIPropertyEditor.java @@ -113,7 +113,13 @@ public class GUIPropertyEditor extends javax.swing.JDialog implements ActionList setLocation(getX()+(noOpen*50), getY()+(noOpen*50)); 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()