diff --git a/de.prob.core/plugin.xml b/de.prob.core/plugin.xml index eaeb084496924b1941929b0cf893552efd41915e..086d193f0a2a734a27fb773347cc52e77f343fc9 100644 --- a/de.prob.core/plugin.xml +++ b/de.prob.core/plugin.xml @@ -30,5 +30,10 @@ kind="string" name="Content of a unit Pragma to send to ProB"> </attributeType> + <attributeType + id="inferredUnitPragma" + kind="string" + name="Content of a unit Pragma received from ProB"> + </attributeType> </extension> </plugin> diff --git a/de.prob.ui/plugin.xml b/de.prob.ui/plugin.xml index f66efd32c39b6ecf6014c2fbbdd0747880da3cc9..0bec42fe738ff764913bffc27f991f2f52067bf3 100644 --- a/de.prob.ui/plugin.xml +++ b/de.prob.ui/plugin.xml @@ -1268,12 +1268,27 @@ <attributeReference descriptionId="de.prob.ui.unitPragma"> </attributeReference> + <attributeReference + descriptionId="de.prob.ui.inferredUnitPragma"> + </attributeReference> </attributeRelation> <attributeRelation elementTypeId="org.eventb.core.constant"> <attributeReference descriptionId="de.prob.ui.unitPragma"> </attributeReference> + <attributeReference + descriptionId="de.prob.ui.inferredUnitPragma"> + </attributeReference> </attributeRelation> + <textAttribute + class="de.prob.ui.pragmas.InferredUnitPragma" + expandsHorizontally="true" + id="de.prob.ui.inferredUnitPragma" + isMath="true" + prefix="Inferred Physical Unit:" + style="de.prob.ui.inferredUnitPragma" + typeId="de.prob.core.inferredUnitPragma"> + </textAttribute> </extension> </plugin> diff --git a/de.prob.ui/src/de/prob/ui/pragmas/InferredUnitPragma.java b/de.prob.ui/src/de/prob/ui/pragmas/InferredUnitPragma.java new file mode 100644 index 0000000000000000000000000000000000000000..2dafdb2230b4a6a1098ba0040b94650fdf58296f --- /dev/null +++ b/de.prob.ui/src/de/prob/ui/pragmas/InferredUnitPragma.java @@ -0,0 +1,74 @@ +/** + * (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich + * Heine Universitaet Duesseldorf This software is licenced under EPL 1.0 + * (http://www.eclipse.org/org/documents/epl-v10.html) + * */ + +package de.prob.ui.pragmas; + +import org.eclipse.core.runtime.IProgressMonitor; +import org.eventb.core.IVariable; +import org.eventb.core.basis.Constant; +import org.eventb.internal.ui.eventbeditor.manipulation.IAttributeManipulation; +import org.rodinp.core.IAttributeType; +import org.rodinp.core.IInternalElement; +import org.rodinp.core.IRodinElement; +import org.rodinp.core.RodinCore; +import org.rodinp.core.RodinDBException; + +import de.prob.core.internal.Activator; + +public class InferredUnitPragma implements IAttributeManipulation { + public static IAttributeType.String ATTRIBUTE = RodinCore + .getStringAttrType(Activator.PLUGIN_ID + ".inferredUnitPragma"); + + public InferredUnitPragma() { + // empty constructor + } + + private IInternalElement asInternalElement(IRodinElement element) { + if (element instanceof IVariable) { + return (IVariable) element; + } else if (element instanceof Constant) { + return (Constant) element; + } + return null; + } + + @Override + public String[] getPossibleValues(IRodinElement element, + IProgressMonitor monitor) { + return new String[] { "", "a", "b", "c" }; + } + + @Override + public String getValue(IRodinElement element, IProgressMonitor monitor) + throws RodinDBException { + return asInternalElement(element).getAttributeValue(ATTRIBUTE); + } + + @Override + public boolean hasValue(IRodinElement element, IProgressMonitor monitor) + throws RodinDBException { + return asInternalElement(element).hasAttribute(ATTRIBUTE); + } + + @Override + public void removeAttribute(IRodinElement element, IProgressMonitor monitor) + throws RodinDBException { + asInternalElement(element).removeAttribute(ATTRIBUTE, monitor); + + } + + @Override + public void setDefaultValue(IRodinElement element, IProgressMonitor monitor) + throws RodinDBException { + asInternalElement(element).setAttributeValue(ATTRIBUTE, "", monitor); + } + + @Override + public void setValue(IRodinElement element, String value, + IProgressMonitor monitor) throws RodinDBException { + asInternalElement(element).setAttributeValue(ATTRIBUTE, value, monitor); + } +}