From 88a10b763d94f2de731b20ae0f91a8030c4cb71b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 7 Jun 2018 12:31:52 +0200 Subject: [PATCH] GUI: In properties tab, support double-click for adding constants, labels Similar to the behaviour in the properties list, if we double-click inside the constant or label table but not on an existing entry, we add a new contant/label line in the table. --- .../userinterface/properties/GUIMultiProperties.java | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 7b6a44a3..0c2e15e4 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -1400,6 +1400,16 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List // there is no property yet, open new property editor a_newProperty(); } + } else if (e.getSource() == consTable || e.getSource() == constantsScroll) { + if (consTable.rowAtPoint(e.getPoint()) == -1) { + // double-click, not an existing row -> add a new constant + a_addConstant(); + } + } else if (e.getSource() == labTable || e.getSource() == labelsScroll) { + if (labTable.rowAtPoint(e.getPoint()) == -1) { + // double-click, not an existing row -> add a new label + a_addLabel(); + } } } }