Browse Source

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
master
Dave Parker 14 years ago
parent
commit
edafa10bbd
  1. 5
      prism/src/userinterface/model/GUIMultiModel.java
  2. 6
      prism/src/userinterface/model/GUIMultiModelHandler.java

5
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

6
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();

Loading…
Cancel
Save