From dbf77a94494ccfd883420cc0c856720dff38e10a Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Wed, 24 Apr 2013 16:56:56 +0200
Subject: [PATCH] store if a model or a context was send to the animator inside
an eclipse service called context_loaded. used to deactivate refinement
checking, etc. for contexts.
---
de.prob.ui/plugin.xml | 51 ++++++++++++++-----
.../prob/ui/eventb/StartAnimationHandler.java | 14 +++++
.../ui/services/ContextLoadedProvider.java | 11 ++++
3 files changed, 62 insertions(+), 14 deletions(-)
create mode 100644 de.prob.ui/src/de/prob/ui/services/ContextLoadedProvider.java
diff --git a/de.prob.ui/plugin.xml b/de.prob.ui/plugin.xml
index 43acbbe7..14cb1e60 100644
--- a/de.prob.ui/plugin.xml
+++ b/de.prob.ui/plugin.xml
@@ -757,27 +757,43 @@
</handler>
<handler
commandId="de.prob.ui.refinement_check">
- <enabledWhen>
- <with
- variable="de.prob.core.model_loaded">
- <equals
- value="enabled">
- </equals>
- </with>
- </enabledWhen>
<class
class="de.prob.ui.refinementcheck.RefinementCheckHandler">
</class>
+ <enabledWhen>
+ <and>
+ <with
+ variable="de.prob.core.model_loaded">
+ <equals
+ value="enabled">
+ </equals>
+ </with>
+ <with
+ variable="de.prob.core.context_loaded">
+ <equals
+ value="disabled">
+ </equals>
+ </with>
+ </and>
+ </enabledWhen>
</handler>
<handler
commandId="de.prob.ui.assertion_check">
<enabledWhen>
- <with
- variable="de.prob.core.model_loaded">
- <equals
- value="enabled">
- </equals>
- </with>
+ <and>
+ <with
+ variable="de.prob.core.model_loaded">
+ <equals
+ value="enabled">
+ </equals>
+ </with>
+ <with
+ variable="de.prob.core.context_loaded">
+ <equals
+ value="disabled">
+ </equals>
+ </with>
+ </and>
</enabledWhen>
<class
class="de.prob.ui.assertion.AssertionCheckHandler">
@@ -1222,6 +1238,13 @@
name="de.prob.ui.ltl.counterexample_loaded"
priorityLevel="workbench">
</variable>
+ </sourceProvider>
+ <sourceProvider
+ provider="de.prob.ui.services.ContextLoadedProvider">
+ <variable
+ name="de.prob.core.context_loaded"
+ priorityLevel="workbench">
+ </variable>
</sourceProvider>
</extension>
</plugin>
diff --git a/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java b/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java
index bad71c48..108ceed9 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/StartAnimationHandler.java
@@ -20,7 +20,9 @@ import org.eclipse.core.runtime.IPath;
import org.eclipse.jface.action.IAction;
import org.eclipse.jface.viewers.ISelection;
import org.eclipse.jface.viewers.IStructuredSelection;
+import org.eclipse.ui.PlatformUI;
import org.eclipse.ui.handlers.HandlerUtil;
+import org.eclipse.ui.services.ISourceProviderService;
import org.eventb.core.IContextRoot;
import org.eventb.core.IEventBRoot;
import org.eventb.core.IMachineRoot;
@@ -33,6 +35,8 @@ import de.prob.core.command.LoadEventBModelCommand;
import de.prob.exceptions.ProBException;
import de.prob.logging.Logger;
import de.prob.ui.PerspectiveFactory;
+import de.prob.ui.services.ContextLoadedProvider;
+import de.prob.ui.services.ModelLoadedProvider;
public class StartAnimationHandler extends AbstractHandler implements IHandler {
@@ -144,6 +148,14 @@ public class StartAnimationHandler extends AbstractHandler implements IHandler {
}
return root;
}
+
+ private void updateContextLoadedProvider(boolean isContext) {
+ ISourceProviderService service = (ISourceProviderService)
+ PlatformUI.getWorkbench().getService(ISourceProviderService.class);
+ ContextLoadedProvider sourceProvider = (ContextLoadedProvider) service
+ .getSourceProvider(ContextLoadedProvider.SERVICE);
+ sourceProvider.setEnabled(isContext);
+ }
private IFile extractResource(final IEventBRoot rootElement) {
IFile resource = null;
@@ -152,9 +164,11 @@ public class StartAnimationHandler extends AbstractHandler implements IHandler {
} else if (rootElement instanceof IMachineRoot) {
resource = ((IMachineRoot) rootElement).getSCMachineRoot()
.getResource();
+ updateContextLoadedProvider(false);
} else if (rootElement instanceof IContextRoot) {
resource = ((IContextRoot) rootElement).getSCContextRoot()
.getResource();
+ updateContextLoadedProvider(true);
}
return resource;
}
diff --git a/de.prob.ui/src/de/prob/ui/services/ContextLoadedProvider.java b/de.prob.ui/src/de/prob/ui/services/ContextLoadedProvider.java
new file mode 100644
index 00000000..5229f7d5
--- /dev/null
+++ b/de.prob.ui/src/de/prob/ui/services/ContextLoadedProvider.java
@@ -0,0 +1,11 @@
+package de.prob.ui.services;
+
+public class ContextLoadedProvider extends AbstractBoolProvider {
+
+ public static final String SERVICE = "de.prob.core.context_loaded";
+
+ public ContextLoadedProvider() {
+ super(SERVICE);
+ }
+
+}
--
GitLab