diff --git a/de.prob.units/plugin.xml b/de.prob.units/plugin.xml index 24f75bf501e63eb2fb344e2ab653ae9a49aebb14..5e63c9174d090fc598b23a6c301cbfe5c848c8eb 100644 --- a/de.prob.units/plugin.xml +++ b/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> diff --git a/de.prob.units/src/de/prob/units/Activator.java b/de.prob.units/src/de/prob/units/Activator.java index cb9482f57446625e611905dd23c999190b96cf5c..fba86f06b5c128daf5aedca07bb8c87e4417c932 100644 --- a/de.prob.units/src/de/prob/units/Activator.java +++ b/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 @@ -13,7 +16,7 @@ public class Activator extends AbstractUIPlugin { // The shared instance private static Activator plugin; - + /** * The constructor */ @@ -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; @@ -40,11 +52,18 @@ public class Activator extends AbstractUIPlugin { /** * Returns the shared instance - * + * * @return the shared instance */ public static Activator getDefault() { return plugin; } + /** + * Registers a file configuration setter for our plugin. + */ + public static void setConfig() { + RodinCore.addElementChangedListener(new ConfSettor()); + } + } diff --git a/de.prob.units/src/de/prob/units/sc/ConfSettor.java b/de.prob.units/src/de/prob/units/sc/ConfSettor.java new file mode 100644 index 0000000000000000000000000000000000000000..1fc7250685ff695aa9c17a690f314e2151a95d1d --- /dev/null +++ b/de.prob.units/src/de/prob/units/sc/ConfSettor.java @@ -0,0 +1,58 @@ +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 diff --git a/de.prob.units/src/de/prob/units/sc/MachineAttributeProcessor.java b/de.prob.units/src/de/prob/units/sc/MachineAttributeProcessor.java new file mode 100644 index 0000000000000000000000000000000000000000..41ea24065944d8611d84b733f647ec7fc37ef76a --- /dev/null +++ b/de.prob.units/src/de/prob/units/sc/MachineAttributeProcessor.java @@ -0,0 +1,31 @@ +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; + } + +}