From 08a8ad01cdea125b4f689d88e2f5845a8256140e Mon Sep 17 00:00:00 2001 From: Mark Kattenbelt Date: Thu, 25 Oct 2007 10:36:37 +0000 Subject: [PATCH] Added warning message when manual exploration is attempted without being in the most recently explored state. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@476 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/simulator/GUISimulator.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 0e2fdef2..4fa490d0 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -136,6 +136,10 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect a_manualUpdate(); currentUpdatesTable.requestFocus(); } + else if (e.getClickCount() == 2 && !currentUpdatesTable.isEnabled()) + { + GUISimulator.this.warning("Simulation", "You cannot continue exploration from the state that is current selected, please select \nthe most recently explored state in the path table first."); + } } });