store if a model or a context was send to the animator inside an eclipse...

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

@@ -757,27 +757,43 @@
       </handler>
       <handler
             commandId="de.prob.ui.refinement_check">
+         <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>
-         <class
-               class="de.prob.ui.refinementcheck.RefinementCheckHandler">
-         </class>
       </handler>
       <handler
             commandId="de.prob.ui.assertion_check">
          <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>
          <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>

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 {
 
@@ -145,6 +149,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;
 		if (rootElement == 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;
 	}

de.prob.ui/src/de/prob/ui/services/ContextLoadedProvider.java

+package de.prob.ui.services;
+
+public class ContextLoadedProvider extends AbstractBoolProvider {
+
+	public static final String SERVICE = "de.prob.core.context_loaded";
+
+	public ContextLoadedProvider() {
+		super(SERVICE);
+	}
+
+}