From 5198f94502d6e67f3bbfb6b2f6192bdf7fa4a808 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 1 Nov 2006 10:35:49 +0000 Subject: [PATCH] Added "new experiment" option to main menu. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@95 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/properties/GUIMultiProperties.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 603df556..0413b2f6 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -1625,6 +1625,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List //ver.setIcon(GUIPrism.getIconFromImage("smallVerify.gif")); propMenu.add(verifySelected); propMenu.add(simulate); + propMenu.add(newExperiment); //ver.add(verifyAll); //propMenu.add(ver); propMenu.setMnemonic('P'); @@ -1955,6 +1956,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List newExperiment.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_N)); newExperiment.putValue(Action.NAME, "New experiment"); newExperiment.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallNew.gif")); + newExperiment.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_F7, 0)); deleteExperiment = new AbstractAction() {