From 447d4732bed04d10f2bcf28ea4a43c4f7da985f3 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 18 Jul 2018 18:37:55 +0100
Subject: [PATCH] GUI: Tooltip hints for creating new
 properties/constant/labels.

---
 prism/src/userinterface/properties/GUIMultiProperties.java | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java
index 7c8d44f1..bab3eb0a 100644
--- a/prism/src/userinterface/properties/GUIMultiProperties.java
+++ b/prism/src/userinterface/properties/GUIMultiProperties.java
@@ -1661,6 +1661,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 							propList = new GUIPropertiesList(getPrism(), this);
 							propList.addListSelectionListener(this);
 							propList.addContainerListener(this);
+							propList.setToolTipText("Double-click or right-click here to create a new property");
 							propScroll.setViewportView(propList);
 						}
 						JScrollPane comScroll = new JScrollPane();
@@ -1680,6 +1681,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 					JSplitPane bottomLeft = new JSplitPane();
 					{
 						constantsScroll = new JScrollPane();
+						constantsScroll.setToolTipText("Double-click or right-click here to create a new constant");
 						{
 							consTable = new GUIPropConstantList(this);
 							consTable.setBackground(Color.white);
@@ -1689,6 +1691,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 							constantsScroll.setBorder(new TitledBorder("Constants"));
 						}
 						labelsScroll = new JScrollPane();
+						labelsScroll.setToolTipText("Double-click or right-click here to create a new label");
 						{
 							labTable = new GUIPropLabelList(this);
 							labTable.setBackground(Color.white);