From 0cf8c8cbe013cd02dcd18833c4c36bbc2c642c10 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 5 Jan 2016 10:09:48 +0000 Subject: [PATCH] GUI: Tweak double-click handling in property list Now, double-clicking on a property will open the editor for that property. Double-clicking on an empty area of the property list will open the "new property" editor. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11109 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../properties/GUIMultiProperties.java | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 50ee64d2..978a6d04 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -36,6 +36,7 @@ import java.awt.Color; import java.awt.Dimension; import java.awt.Font; import java.awt.GridLayout; +import java.awt.Rectangle; import java.awt.Toolkit; import java.awt.datatransfer.Clipboard; import java.awt.datatransfer.DataFlavor; @@ -1376,9 +1377,22 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List int index = propList.locationToIndex(e.getPoint()); if (index != -1) { - propList.setSelectedIndex(index); + // locationToIndex provides the index to the "nearest" + // property. We check here if the cursor is actually on + // the property. + Rectangle bounds = propList.getCellBounds(index, index); + if (bounds != null && bounds.contains(e.getPoint())) { + // Cursor is on the property: select and open editor + propList.setSelectedIndex(index); + a_editProperty(); + } else { + // Cursor is not on the property: open new property editor + a_newProperty(); + } + } else { + // there is no property yet, open new property editor + a_newProperty(); } - a_editProperty(); } } }