add a second text field to output the inferred pragma

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>

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>

de.prob.ui/src/de/prob/ui/pragmas/InferredUnitPragma.java

+/**
+ * (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);
+	}
+}