working on static checking of machine variables (copy over attribute), infrastructure done

de.prob.units/plugin.xml

@@ -98,4 +98,27 @@
             name="Content of a unit Pragma received from ProB">
       </attributeType>
    </extension>
+   <extension
+         point="org.eventb.core.configurations">
+      <configuration
+            id="mchBase"
+            name="mchBase">
+         <scModule
+               id="de.prob.units.machineAttributeProcessor">
+         </scModule>
+      </configuration>
+   </extension>
+   <extension
+         id="scMachineModuleTypes"
+         point="org.eventb.core.scModuleTypes">
+      <processorType
+            class="de.prob.units.sc.MachineAttributeProcessor"
+            id="machineAttributeProcessor"
+            name="machineAttributeProcessor"
+            parent="org.eventb.core.machineModule">
+         <prereq
+               id="org.eventb.core.machineVariableModule">
+         </prereq>
+      </processorType>
+   </extension>
 </plugin>

de.prob.units/src/de/prob/units/Activator.java

@@ -2,6 +2,9 @@ package de.prob.units;
 
 import org.eclipse.ui.plugin.AbstractUIPlugin;
 import org.osgi.framework.BundleContext;
+import org.rodinp.core.RodinCore;
+
+import de.prob.units.sc.ConfSettor;
 
 /**
  * The activator class controls the plug-in life cycle
@@ -22,16 +25,25 @@ public class Activator extends AbstractUIPlugin {
 
 	/*
 	 * (non-Javadoc)
-	 * @see org.eclipse.ui.plugin.AbstractUIPlugin#start(org.osgi.framework.BundleContext)
+	 * 
+	 * @see
+	 * org.eclipse.ui.plugin.AbstractUIPlugin#start(org.osgi.framework.BundleContext
+	 * )
 	 */
 	public void start(BundleContext context) throws Exception {
 		super.start(context);
 		plugin = this;
+
+		setConfig();
+
 	}
 
 	/*
 	 * (non-Javadoc)
-	 * @see org.eclipse.ui.plugin.AbstractUIPlugin#stop(org.osgi.framework.BundleContext)
+	 * 
+	 * @see
+	 * org.eclipse.ui.plugin.AbstractUIPlugin#stop(org.osgi.framework.BundleContext
+	 * )
 	 */
 	public void stop(BundleContext context) throws Exception {
 		plugin = null;
@@ -47,4 +59,11 @@ public class Activator extends AbstractUIPlugin {
 		return plugin;
 	}
 
+	/**
+	 * Registers a file configuration setter for our plugin.
+	 */
+	public static void setConfig() {
+		RodinCore.addElementChangedListener(new ConfSettor());
+	}
+
 }

de.prob.units/src/de/prob/units/sc/ConfSettor.java

+package de.prob.units.sc;
+
+import org.eventb.core.IMachineRoot;
+import org.rodinp.core.ElementChangedEvent;
+import org.rodinp.core.IElementChangedListener;
+import org.rodinp.core.IElementType;
+import org.rodinp.core.IInternalElement;
+import org.rodinp.core.IRodinDB;
+import org.rodinp.core.IRodinElement;
+import org.rodinp.core.IRodinElementDelta;
+import org.rodinp.core.IRodinFile;
+import org.rodinp.core.IRodinProject;
+import org.rodinp.core.RodinDBException;
+
+import de.prob.units.Activator;
+
+/**
+ * Class that updates the configuration of files, to add the static checker
+ * modules for our qualitative probabilistic reasoning plug-in.
+ */
+public class ConfSettor implements IElementChangedListener {
+
+	private static final String CONFIG = Activator.PLUGIN_ID + ".mchBase";
+
+	public void elementChanged(ElementChangedEvent event) {
+
+		final IRodinElementDelta d = event.getDelta();
+		try {
+			processDelta(d);
+		} catch (final RodinDBException e) {
+			// TODO add exception log
+		}
+	}
+
+	private void processDelta(final IRodinElementDelta d)
+			throws RodinDBException {
+		final IRodinElement e = d.getElement();
+
+		final IElementType<? extends IRodinElement> elementType = e
+				.getElementType();
+		if (elementType.equals(IRodinDB.ELEMENT_TYPE)
+				|| elementType.equals(IRodinProject.ELEMENT_TYPE)) {
+			for (final IRodinElementDelta de : d.getAffectedChildren()) {
+				processDelta(de);
+			}
+		} else if (elementType.equals(IRodinFile.ELEMENT_TYPE)) {
+			final IInternalElement root = ((IRodinFile) e).getRoot();
+
+			if (root.getElementType().equals(IMachineRoot.ELEMENT_TYPE)) {
+				final IMachineRoot mch = (IMachineRoot) root;
+				final String conf = mch.getConfiguration();
+				if (!conf.contains(CONFIG)) {
+					mch.setConfiguration(conf + ";" + CONFIG, null);
+				}
+			}
+		}
+	}
+}
\ No newline at end of file

de.prob.units/src/de/prob/units/sc/MachineAttributeProcessor.java

+package de.prob.units.sc;
+
+import org.eclipse.core.runtime.CoreException;
+import org.eclipse.core.runtime.IProgressMonitor;
+import org.eventb.core.sc.SCCore;
+import org.eventb.core.sc.SCProcessorModule;
+import org.eventb.core.sc.state.ISCStateRepository;
+import org.eventb.core.tool.IModuleType;
+import org.rodinp.core.IInternalElement;
+import org.rodinp.core.IRodinElement;
+
+import de.prob.units.Activator;
+
+public class MachineAttributeProcessor extends SCProcessorModule {
+	public static final IModuleType<MachineAttributeProcessor> MODULE_TYPE = SCCore
+			.getModuleType(Activator.PLUGIN_ID + ".machineAttributeProcessor"); //$NON-NLS-1$
+
+	@Override
+	public void process(IRodinElement element, IInternalElement target,
+			ISCStateRepository repository, IProgressMonitor monitor)
+			throws CoreException {
+		System.out.println("blah");
+
+	}
+
+	@Override
+	public IModuleType<?> getModuleType() {
+		return MODULE_TYPE;
+	}
+
+}