From edafa10bbdaaa9b6a36530d61cca245732fc411e Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 21 Mar 2012 09:31:30 +0000
Subject: [PATCH] GUI fix: model errors (and jumping to that tab) work better
 with running experiments.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4922 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/userinterface/model/GUIMultiModel.java        | 5 +++++
 prism/src/userinterface/model/GUIMultiModelHandler.java | 6 +++++-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/prism/src/userinterface/model/GUIMultiModel.java b/prism/src/userinterface/model/GUIMultiModel.java
index f40b84d1..0bce3c11 100644
--- a/prism/src/userinterface/model/GUIMultiModel.java
+++ b/prism/src/userinterface/model/GUIMultiModel.java
@@ -129,6 +129,11 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener
 		return popup;
 	}
 
+	public boolean getComputing()
+	{
+		return computing;
+	}
+	
 	public void doEnables()
 	{
 		// do nothing if not initialised yet
diff --git a/prism/src/userinterface/model/GUIMultiModelHandler.java b/prism/src/userinterface/model/GUIMultiModelHandler.java
index ea06207e..a61e8929 100644
--- a/prism/src/userinterface/model/GUIMultiModelHandler.java
+++ b/prism/src/userinterface/model/GUIMultiModelHandler.java
@@ -849,6 +849,7 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener
 		{
 			public void run()
 			{
+				editor.modelParseSuccessful();
 				updateBuiltModelDisplay();
 				theModel.doEnables();
 				theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODEL_BUILT, lastMFConstants));
@@ -889,7 +890,10 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener
 			{
 				if (lastBuildError != null && lastBuildError instanceof PrismLangException) {
 					editor.modelParseFailed((PrismLangException) lastBuildError, false);
-					theModel.tabToFront();
+					// Bring model tab to front, but only if not busy e.g. with experiment
+					if (!theModel.getComputing()) {
+						theModel.tabToFront();
+					}
 				}
 				updateBuiltModelDisplay();
 				theModel.doEnables();