Remove no longer used units plugin code

The units plugin has been disabled since 2019
(47bc301e) and the Prolog side no longer
supports it.

de.prob.core/src/de/prob/core/command/ActivateUnitPluginCommand.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.core.command;
-
-import de.prob.core.Animator;
-import de.prob.exceptions.ProBException;
-import de.prob.parser.ISimplifiedROMap;
-import de.prob.prolog.output.IPrologTermOutput;
-import de.prob.prolog.term.PrologTerm;
-
-public class ActivateUnitPluginCommand implements IComposableCommand {
-
-	private static final ActivateCmd ACTIVATE_CMD = new ActivateCmd();
-	private final GetPrologRandomSeed getRandomSeed;
-	private final ComposedCommand cmd;
-
-	public ActivateUnitPluginCommand() {
-		this.getRandomSeed = new GetPrologRandomSeed();
-		this.cmd = new ComposedCommand(getRandomSeed, ACTIVATE_CMD);
-	}
-
-	public static void activateUnitPlugin(final Animator animator)
-			throws ProBException {
-		animator.execute(new ActivateUnitPluginCommand());
-	}
-
-	public void processResult(
-			final ISimplifiedROMap<String, PrologTerm> bindings)
-			throws CommandException {
-		cmd.processResult(bindings);
-		final Animator animator = Animator.getAnimator();
-		animator.setRandomSeed(getRandomSeed.getSeed());
-	}
-
-	public void writeCommand(final IPrologTermOutput pto)
-			throws CommandException {
-		cmd.writeCommand(pto);
-	}
-
-	private final static class ActivateCmd implements IComposableCommand {
-		public void processResult(
-				final ISimplifiedROMap<String, PrologTerm> bindings)
-				throws CommandException {
-		}
-
-		public void writeCommand(final IPrologTermOutput pto) {
-			pto.openTerm("activate_plugin");
-			pto.printAtom("units");
-			pto.closeTerm();
-		}
-	}
-
-}

de.prob.core/src/de/prob/core/command/GetPluginResultCommand.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.core.command;
-
-import de.prob.parser.BindingGenerator;
-import de.prob.parser.ISimplifiedROMap;
-import de.prob.parser.ResultParserException;
-import de.prob.prolog.output.IPrologTermOutput;
-import de.prob.prolog.term.CompoundPrologTerm;
-import de.prob.prolog.term.PrologTerm;
-
-public final class GetPluginResultCommand implements IComposableCommand {
-
-	private final String resultID;
-	private CompoundPrologTerm result;
-
-	public GetPluginResultCommand(final String resultID) {
-		this.resultID = resultID;
-	}
-
-	public CompoundPrologTerm getResult() {
-		return result;
-	}
-
-	@Override
-	public void processResult(
-			final ISimplifiedROMap<String, PrologTerm> bindings)
-			throws CommandException {
-		try {
-			result = BindingGenerator.getCompoundTerm(bindings.get("Bindings"),
-					1);
-		} catch (ResultParserException e) {
-			CommandException commandException = new CommandException(
-					e.getLocalizedMessage(), e);
-			commandException.notifyUserOnce();
-			throw commandException;
-		}
-	}
-
-	@Override
-	public void writeCommand(final IPrologTermOutput pto) {
-		pto.openTerm("get_plugin_output").printAtomOrNumber(resultID)
-				.printVariable("Bindings").closeTerm();
-	}
-
-}

de.prob.units.tests/.classpath

-<?xml version="1.0" encoding="UTF-8"?>
-<classpath>
-	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
-	<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
-	<classpathentry kind="src" path="src"/>
-	<classpathentry kind="output" path="bin"/>
-</classpath>

de.prob.units.tests/.project

-<?xml version="1.0" encoding="UTF-8"?>
-<projectDescription>
-	<name>de.prob.units.tests</name>
-	<comment></comment>
-	<projects>
-	</projects>
-	<buildSpec>
-		<buildCommand>
-			<name>org.eclipse.jdt.core.javabuilder</name>
-			<arguments>
-			</arguments>
-		</buildCommand>
-		<buildCommand>
-			<name>org.eclipse.pde.ManifestBuilder</name>
-			<arguments>
-			</arguments>
-		</buildCommand>
-		<buildCommand>
-			<name>org.eclipse.pde.SchemaBuilder</name>
-			<arguments>
-			</arguments>
-		</buildCommand>
-	</buildSpec>
-	<natures>
-		<nature>org.eclipse.pde.PluginNature</nature>
-		<nature>org.eclipse.jdt.core.javanature</nature>
-	</natures>
-</projectDescription>

de.prob.units.tests/.settings/org.eclipse.jdt.core.prefs

-eclipse.preferences.version=1
-org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
-org.eclipse.jdt.core.compiler.compliance=1.8
-org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
-org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
-org.eclipse.jdt.core.compiler.source=1.8

de.prob.units.tests/META-INF/MANIFEST.MF

-Manifest-Version: 1.0
-Bundle-ManifestVersion: 2
-Bundle-Name: Tests
-Bundle-SymbolicName: de.prob.units.tests
-Bundle-Version: 1.0.0.qualifier
-Bundle-Activator: de.prob.units.tests.Activator
-Require-Bundle: org.eclipse.ui,
- org.eclipse.core.runtime,
- de.prob.units;bundle-version="1.0.0",
- org.junit;bundle-version="4.8.2",
- org.rodinp.core;bundle-version="[1.3.1,1.7.0)",
- de.prob.core;bundle-version="9.3.0",
- org.eventb.core;bundle-version="[2.1.0,2.6.0)"
-Bundle-ActivationPolicy: lazy
-Bundle-RequiredExecutionEnvironment: JavaSE-1.8

de.prob.units.tests/build.properties

-source.. = src/
-output.. = bin/
-bin.includes = META-INF/,\
-               .

de.prob.units.tests/src/de/prob/units/pragmas/tests/PragmaAttributesTest.java

-package de.prob.units.pragmas.tests;
-
-import org.eclipse.core.resources.IncrementalProjectBuilder;
-import org.eclipse.core.runtime.CoreException;
-import org.eclipse.core.runtime.NullProgressMonitor;
-import org.eventb.core.IConstant;
-import org.eventb.core.IContextRoot;
-import org.eventb.core.IEventBProject;
-import org.eventb.core.IMachineRoot;
-import org.eventb.core.IVariable;
-import org.junit.Test;
-import org.rodinp.core.IAttributeType;
-import org.rodinp.core.RodinCore;
-
-import de.prob.core.translator.TranslationFailedException;
-import de.prob.units.tests.AbstractEventBTests;
-
-public class PragmaAttributesTest extends AbstractEventBTests {
-	final IAttributeType.String UNITATTRIBUTE = RodinCore
-			.getStringAttrType("de.prob.units.unitPragmaAttribute");
-
-	@Test
-	public void testMachineWithUnitPragmaOnVariable() throws CoreException,
-			TranslationFailedException {
-		IEventBProject project = createEventBProject("TestProject");
-		IMachineRoot machine = createMachine(project, "TestMachine");
-
-		IVariable v1 = createVariable(machine, "v1");
-		createInvariant(machine, "inv1", "v1=5", false);
-
-		// add unit pragma to variable
-		v1.setAttributeValue(UNITATTRIBUTE, "test", new NullProgressMonitor());
-
-		// save file and build workspace - this triggers static check, and
-		// generates missing files
-		machine.getRodinFile().save(monitor, false);
-		workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor);
-
-		// there should be one variable and one SC variable
-		assertEquals(1, machine.getVariables().length);
-		assertEquals(1, machine.getSCMachineRoot().getSCVariables().length);
-
-		// and both should hold our attribute
-		assertEquals("test",
-				machine.getVariables()[0].getAttributeValue(UNITATTRIBUTE));
-		assertEquals("test",
-				machine.getSCMachineRoot().getSCVariables()[0]
-						.getAttributeValue(UNITATTRIBUTE));
-	}
-
-	@Test
-	public void testContextWithUnitPragmaOnConstant() throws CoreException,
-			TranslationFailedException {
-		IEventBProject project = createEventBProject("TestProject");
-		IContextRoot context = createContext(project, "TestContext");
-
-		IConstant c1 = createConstant(context, "cst1");
-		createAxiom(context, "axm1", "cst1=5", false);
-
-		// add unit pragma to constant
-		c1.setAttributeValue(UNITATTRIBUTE, "test", new NullProgressMonitor());
-
-		// save file and build workspace - this triggers static check, and
-		// generates missing files
-		context.getRodinFile().save(monitor, false);
-		workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor);
-
-		// there should be one constant and one SC constant
-		// both holding the attribute
-		assertEquals(1, context.getConstants().length);
-		assertEquals(1, context.getSCContextRoot().getSCConstants().length);
-
-		// and both should hold our attribute
-		assertEquals("test",
-				context.getConstants()[0].getAttributeValue(UNITATTRIBUTE));
-		assertEquals("test",
-				context.getSCContextRoot().getSCConstants()[0]
-						.getAttributeValue(UNITATTRIBUTE));
-
-	}
-}

de.prob.units.tests/src/de/prob/units/pragmas/tests/ReplacesEventBSyntaxTest.java

-package de.prob.units.pragmas.tests;
-
-import org.eclipse.core.resources.IncrementalProjectBuilder;
-import org.eclipse.core.runtime.CoreException;
-import org.eclipse.core.runtime.NullProgressMonitor;
-import org.eventb.core.IConstant;
-import org.eventb.core.IContextRoot;
-import org.eventb.core.IEventBProject;
-import org.eventb.core.IMachineRoot;
-import org.eventb.core.IVariable;
-import org.junit.Test;
-import org.rodinp.core.IAttributeType;
-import org.rodinp.core.RodinCore;
-
-import de.prob.core.translator.TranslationFailedException;
-import de.prob.units.tests.AbstractEventBTests;
-
-public class ReplacesEventBSyntaxTest extends AbstractEventBTests {
-	final IAttributeType.String UNITATTRIBUTE = RodinCore
-			.getStringAttrType("de.prob.units.unitPragmaAttribute");
-
-	@Test
-	public void testReplacesOnVariable() throws CoreException,
-			TranslationFailedException {
-		IEventBProject project = createEventBProject("TestProject");
-		IMachineRoot machine = createMachine(project, "TestMachine");
-
-		IVariable v1 = createVariable(machine, "v1");
-		createInvariant(machine, "inv1", "v1=5", false);
-
-		// add unit pragma to variable
-		v1.setAttributeValue(UNITATTRIBUTE, "m^2", new NullProgressMonitor());
-
-		// save file and build workspace - this triggers static check, and
-		// generates missing files
-		machine.getRodinFile().save(monitor, false);
-		workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor);
-
-		assertEquals("m^2",
-				machine.getVariables()[0].getAttributeValue(UNITATTRIBUTE));
-		assertEquals("m**2",
-				machine.getSCMachineRoot().getSCVariables()[0]
-						.getAttributeValue(UNITATTRIBUTE));
-	}
-
-	@Test
-	public void testReplacesOnConstant() throws CoreException,
-			TranslationFailedException {
-		IEventBProject project = createEventBProject("TestProject");
-		IContextRoot context = createContext(project, "TestContext");
-
-		IConstant c1 = createConstant(context, "cst1");
-		createAxiom(context, "axm1", "cst1=5", false);
-
-		// add unit pragma to constant
-		c1.setAttributeValue(UNITATTRIBUTE, "m^2", new NullProgressMonitor());
-
-		// save file and build workspace - this triggers static check, and
-		// generates missing files
-		context.getRodinFile().save(monitor, false);
-		workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor);
-
-		assertEquals("m^2",
-				context.getConstants()[0].getAttributeValue(UNITATTRIBUTE));
-		assertEquals("m**2",
-				context.getSCContextRoot().getSCConstants()[0]
-						.getAttributeValue(UNITATTRIBUTE));
-
-	}
-}

de.prob.units.tests/src/de/prob/units/tests/AbstractTests.java

-package de.prob.units.tests;
-
-import java.util.Collection;
-import java.util.Map;
-import java.util.Set;
-
-import junit.framework.TestCase;
-
-/**
- * @author htson
- *         <p>
- *         This abstract class contains utility methods supporting testing.
- *         </p>
- */
-public abstract class AbstractTests extends TestCase {
-
-	/**
-	 * Constructor: Create max_size test case.
-	 */
-	public AbstractTests() {
-		super();
-	}
-
-	/**
-	 * Constructor: Create max_size test case with the given name.
-	 * 
-	 * @param name
-	 *            the name of test
-	 */
-	public AbstractTests(String name) {
-		super(name);
-	}
-
-	/**
-	 * Utility method to compare two string collections. The expected collection
-	 * is given in terms of an array of strings. The actual collection is given
-	 * as a collection of strings. The two are the same if the number of
-	 * elements is the same and every element of the expected collection appear
-	 * in the actual collection.
-	 * 
-	 * @param msg
-	 *            a message.
-	 * @param actual
-	 *            actual collection of strings.
-	 * @param expected
-	 *            expected array of strings.
-	 */
-	protected static void assertSameStrings(String msg,
-			Collection<String> actual, String... expected) {
-		assertEquals(msg + ": Incorrect number of elements\n", expected.length,
-				actual.size());
-		for (String exp : expected) {
-			assertTrue(msg + ": Expected element " + exp + " not found",
-					actual.contains(exp));
-		}
-	}
-
-	/**
-	 * Utility method to compare two arrays of strings. The two are the same if
-	 * the number of elements is the same, and the strings at the same index are
-	 * the same.
-	 * 
-	 * @param msg
-	 *            a message.
-	 * @param actual
-	 *            actual array of strings.
-	 * @param expected
-	 *            expected array of strings.
-	 */
-	protected static void assertSameStrings(String msg, String[] actual,
-			String... expected) {
-		assertEquals(msg + ": Incorrect number of strings\n", expected.length,
-				actual.length);
-		for (int i = 0; i < expected.length; i++) {
-			assertEquals(msg, expected[i], actual[i]);
-		}
-	}
-
-	/**
-	 * Utility method to compare two arrays of objects. The two are the same if
-	 * the number of elements is the same, and the objects at the same index are
-	 * the same.
-	 * 
-	 * @param msg
-	 *            a message.
-	 * @param expected
-	 *            expected array of objects.
-	 * @param actual
-	 *            actual array of objects.
-	 */
-	protected static void assertSameObjects(String msg, Object[] expected,
-			Object[] actual) {
-		assertEquals(msg + ": Incorrect number of objects\n", expected.length,
-				actual.length);
-		for (int i = 0; i < expected.length; i++) {
-			assertEquals(msg, expected[i], actual[i]);
-		}
-	}
-
-	/**
-	 * Utility method to compare two maps of objects to objects. The two are the
-	 * same if the key sets are the same (using
-	 * {@link #assertSameSet(String, Set, Set)}), and for each key, they map to
-	 * the same value.
-	 * 
-	 * @param msg
-	 *            a messages.
-	 * @param expected
-	 *            expected map.
-	 * @param actual
-	 *            actual map.
-	 */
-	protected void assertSameMap(String msg,
-			Map<? extends Object, ? extends Object> expected,
-			Map<? extends Object, ? extends Object> actual) {
-		Set<? extends Object> expectedKeySet = expected.keySet();
-		Set<? extends Object> actualKeySet = actual.keySet();
-		assertSameSet(msg, expectedKeySet, actualKeySet);
-		for (Object key : expectedKeySet) {
-			assertEquals(msg, expected.get(key), actual.get(key));
-		}
-	}
-
-	/**
-	 * Utility method to compare two sets of objects. The two are the same if
-	 * they have the same number of elements, and each element of the expected
-	 * set appears in the actual set.
-	 * 
-	 * @param msg
-	 * @param expected
-	 * @param actual
-	 */
-	protected void assertSameSet(String msg, Set<? extends Object> expected,
-			Set<? extends Object> actual) {
-		assertEquals(msg + ": The number of elements must be the same",
-				expected.size(), actual.size());
-		for (Object elm : expected) {
-			assertTrue(msg + ": expected element " + elm + " not found",
-					actual.contains(elm));
-		}
-	}
-
-}
\ No newline at end of file

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

-package de.prob.units.tests;
-
-import org.eclipse.ui.plugin.AbstractUIPlugin;
-import org.osgi.framework.BundleContext;
-
-/**
- * The activator class controls the plug-in life cycle
- */
-public class Activator extends AbstractUIPlugin {
-
-	// The plug-in ID
-	public static final String PLUGIN_ID = "de.prob.units.tests"; //$NON-NLS-1$
-
-	// The shared instance
-	private static Activator plugin;
-	
-	/**
-	 * The constructor
-	 */
-	public Activator() {
-	}
-
-	/*
-	 * (non-Javadoc)
-	 * @see org.eclipse.ui.plugin.AbstractUIPlugin#start(org.osgi.framework.BundleContext)
-	 */
-	public void start(BundleContext context) throws Exception {
-		super.start(context);
-		plugin = this;
-	}
-
-	/*
-	 * (non-Javadoc)
-	 * @see org.eclipse.ui.plugin.AbstractUIPlugin#stop(org.osgi.framework.BundleContext)
-	 */
-	public void stop(BundleContext context) throws Exception {
-		plugin = null;
-		super.stop(context);
-	}
-
-	/**
-	 * Returns the shared instance
-	 *
-	 * @return the shared instance
-	 */
-	public static Activator getDefault() {
-		return plugin;
-	}
-
-}

de.prob.units.tests/src/de/prob/units/translation/tests/PragmaTranslatorTest.java

-package de.prob.units.translation.tests;
-
-import java.io.PrintWriter;
-import java.io.StringWriter;
-
-import org.eclipse.core.resources.IncrementalProjectBuilder;
-import org.eclipse.core.runtime.CoreException;
-import org.eclipse.core.runtime.NullProgressMonitor;
-import org.eventb.core.IConstant;
-import org.eventb.core.IContextRoot;
-import org.eventb.core.IEventBProject;
-import org.eventb.core.IMachineRoot;
-import org.eventb.core.IVariable;
-import org.junit.Before;
-import org.junit.Test;
-import org.rodinp.core.IAttributeType;
-import org.rodinp.core.RodinCore;
-
-import de.prob.core.translator.TranslationFailedException;
-import de.prob.eventb.translator.TranslatorFactory;
-import de.prob.units.tests.AbstractEventBTests;
-
-public class PragmaTranslatorTest extends AbstractEventBTests {
-	final IAttributeType.String UNITATTRIBUTE = RodinCore
-			.getStringAttrType("de.prob.units.unitPragmaAttribute");
-
-	private StringWriter stringWriter;
-	private PrintWriter writer;
-
-	@Before
-	@Override
-	protected void setUp() throws Exception {
-		super.setUp();
-		stringWriter = new StringWriter();
-		writer = new PrintWriter(stringWriter);
-	}
-
-	@Test
-	public void testMachineWithUnitPragmaOnVariable() throws CoreException,
-			TranslationFailedException {
-		IEventBProject project = createEventBProject("TestProject");
-		IMachineRoot machine = createMachine(project, "TestMachine");
-
-		IVariable v1 = createVariable(machine, "v1");
-		createInvariant(machine, "inv1", "v1=5", false);
-
-		// add unit pragma to variable
-		v1.setAttributeValue(UNITATTRIBUTE, "test", new NullProgressMonitor());
-
-		// save file and build workspace - this triggers static check, and
-		// generates missing files
-		machine.getRodinFile().save(monitor, false);
-		workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor);
-
-		// there should be one variable and one SC variable
-		assertEquals(1, machine.getVariables().length);
-		assertEquals(1, machine.getSCMachineRoot().getSCVariables().length);
-
-		TranslatorFactory.translate(machine, writer);
-
-		assertEquals(
-				"package(load_event_b_project([event_b_model(none,'TestMachine',[sees(none,[]),variables(none,[identifier(none,v1)]),invariant(none,[equal(rodinpos('TestMachine',inv1,'('),identifier(none,v1),integer(none,5))]),theorems(none,[]),events(none,[])])],[],[exporter_version(2),pragma(unit,'TestMachine',v1,[test])],_Error)).\n",
-				stringWriter.getBuffer().toString());
-	}
-
-	@Test
-	public void testContextWithUnitPragmaOnConstant() throws CoreException,
-			TranslationFailedException {
-		IEventBProject project = createEventBProject("TestProject");
-		IContextRoot context = createContext(project, "TestContext");
-
-		IConstant c1 = createConstant(context, "cst1");
-		createAxiom(context, "axm1", "cst1=5", false);
-
-		// add unit pragma to constant
-		c1.setAttributeValue(UNITATTRIBUTE, "test", new NullProgressMonitor());
-
-		// save file and build workspace - this triggers static check, and
-		// generates missing files
-		context.getRodinFile().save(monitor, false);
-		project.getRodinProject().save(monitor, false);
-		workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor);
-
-		// there should be one constant and one SC constant
-		assertEquals(1, context.getConstants().length);
-		assertEquals(1, context.getSCContextRoot().getSCConstants().length);
-
-		TranslatorFactory.translate(context, writer);
-
-		assertEquals(
-				"package(load_event_b_project([],[event_b_context(none,'TestContext',[extends(none,[]),constants(none,[identifier(none,cst1)]),axioms(none,[equal(rodinpos('TestContext',axm1,'('),identifier(none,cst1),integer(none,5))]),theorems(none,[]),sets(none,[])])],[exporter_version(2),pragma(unit,'TestContext',cst1,[test])],_Error)).\n",
-				stringWriter.getBuffer().toString());
-	}
-}

de.prob.units/.classpath

-<?xml version="1.0" encoding="UTF-8"?>
-<classpath>
-	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
-	<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
-	<classpathentry kind="src" path="src"/>
-	<classpathentry kind="output" path="bin"/>
-</classpath>

de.prob.units/.project

-<?xml version="1.0" encoding="UTF-8"?>
-<projectDescription>
-	<name>de.prob.units</name>
-	<comment></comment>
-	<projects>
-	</projects>
-	<buildSpec>
-		<buildCommand>
-			<name>org.eclipse.jdt.core.javabuilder</name>
-			<arguments>
-			</arguments>
-		</buildCommand>
-		<buildCommand>
-			<name>org.eclipse.pde.ManifestBuilder</name>
-			<arguments>
-			</arguments>
-		</buildCommand>
-		<buildCommand>
-			<name>org.eclipse.pde.SchemaBuilder</name>
-			<arguments>
-			</arguments>
-		</buildCommand>
-	</buildSpec>
-	<natures>
-		<nature>org.eclipse.pde.PluginNature</nature>
-		<nature>org.eclipse.jdt.core.javanature</nature>
-	</natures>
-</projectDescription>

de.prob.units/.settings/org.eclipse.jdt.core.prefs

-eclipse.preferences.version=1
-org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
-org.eclipse.jdt.core.compiler.compliance=1.8
-org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
-org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
-org.eclipse.jdt.core.compiler.source=1.8

de.prob.units/META-INF/MANIFEST.MF

-Manifest-Version: 1.0
-Bundle-ManifestVersion: 2
-Bundle-Name: ProB Physical Units Support
-Bundle-SymbolicName: de.prob.units;singleton:=true
-Bundle-Version: 7.4.2.qualifier
-Bundle-Activator: de.prob.units.Activator
-Require-Bundle: org.eclipse.core.runtime,
- org.eclipse.core.commands,
- org.eclipse.core.resources,
- org.eclipse.jface,
- org.rodinp.core;bundle-version="[1.7.0,2.0.0)",
- de.prob.core;bundle-version="[9.4.0,9.5.0)",
- org.eventb.ui;bundle-version="[3.0.0,4.0.0)",
- de.prob.ui;bundle-version="[7.4.0,7.5.0)",
- org.eventb.core;bundle-version="[3.0.0,4.0.0)",
- org.eclipse.ui.workbench
-Bundle-ActivationPolicy: lazy
-Bundle-RequiredExecutionEnvironment: JavaSE-1.8
-Bundle-Vendor: HHU Düsseldorf STUPS Group

de.prob.units/build.properties

-source.. = src/
-output.. = bin/
-bin.includes = META-INF/,\
-               .,\
-               icons/,\
-               plugin.xml

de.prob.units/plugin.xml

-<?xml version="1.0" encoding="UTF-8"?>
-<?eclipse version="3.4"?>
-<plugin>
-   <extension
-         point="org.eventb.ui.editorItems">
-      <textAttribute
-            class="de.prob.units.pragmas.UnitPragmaAttribute"
-            expandsHorizontally="false"
-            id="de.prob.units.unitPragmaAttribute"
-            isMath="true"
-            prefix="Physical Unit:"
-            style="single"
-            typeId="de.prob.units.unitPragmaAttribute">
-      </textAttribute>
-      <attributeRelation
-            elementTypeId="org.eventb.core.variable">
-         <attributeReference
-               descriptionId="de.prob.units.unitPragmaAttribute">
-         </attributeReference>
-         <attributeReference
-               descriptionId="de.prob.units.inferredUnitPragmaAttribute">
-         </attributeReference>
-      </attributeRelation>
-      <attributeRelation
-            elementTypeId="org.eventb.core.constant">
-         <attributeReference
-               descriptionId="de.prob.units.unitPragmaAttribute">
-         </attributeReference>
-         <attributeReference
-               descriptionId="de.prob.units.inferredUnitPragmaAttribute">
-         </attributeReference>
-      </attributeRelation>
-      <textAttribute
-            class="de.prob.units.pragmas.InferredUnitPragmaAttribute"
-            expandsHorizontally="false"
-            id="de.prob.units.inferredUnitPragmaAttribute"
-            isMath="true"
-            prefix="Inferred Physical Unit:"
-            style="single"
-            typeId="de.prob.units.inferredUnitPragmaAttribute">
-      </textAttribute>
-      <attributeRelation
-            elementTypeId="org.eventb.core.scVariable">
-         <attributeReference
-               descriptionId="de.prob.units.unitPragmaAttribute">
-         </attributeReference>
-         <attributeReference
-               descriptionId="de.prob.units.inferredUnitPragmaAttribute">
-         </attributeReference>
-      </attributeRelation>
-      <attributeRelation
-            elementTypeId="org.eventb.core.scConstant">
-         <attributeReference
-               descriptionId="de.prob.units.unitPragmaAttribute">
-         </attributeReference>
-         <attributeReference
-               descriptionId="de.prob.units.inferredUnitPragmaAttribute">
-         </attributeReference>
-      </attributeRelation>
-   </extension>
-   <extension
-         point="org.eclipse.ui.handlers">
-      <handler
-            class="de.prob.units.ui.StartUnitAnalysisHandler"
-            commandId="de.prob.units.startunitanalysis">
-      </handler>
-   </extension>
-   <extension
-         point="org.eclipse.ui.menus">
-      <menuContribution
-            locationURI="popup:fr.systerel.explorer.navigator.view">
-         <separator
-               name="de.prob.units.separator2"
-               visible="true">
-         </separator>
-         <command
-               commandId="de.prob.units.startunitanalysis"
-               icon="icons/unit_analysis.png"
-               label="Analyse Physical Units"
-               style="push">
-            <visibleWhen>
-               <with
-                     variable="selection">
-                  <iterate
-                        operator="or">
-                     <or>
-                        <instanceof
-                              value="org.eventb.core.IMachineRoot">
-                        </instanceof>
-                        <instanceof
-                              value="org.eventb.core.IContextRoot">
-                        </instanceof>
-                     </or>
-                  </iterate>
-               </with>
-            </visibleWhen>
-         </command>
-         <separator
-               name="de.prob.units.separator1"
-               visible="true">
-         </separator>
-      </menuContribution>
-   </extension>
-   <extension
-         point="org.eclipse.ui.commands">
-      <command
-            id="de.prob.units.startunitanalysis"
-            name="Analyse Physical Units">
-      </command>
-   </extension>
-   <extension
-         point="org.rodinp.core.attributeTypes">
-      <attributeType
-            id="unitPragmaAttribute"
-            kind="string"
-            name="Content of a unit Pragma to send to ProB">
-      </attributeType>
-      <attributeType
-            id="inferredUnitPragmaAttribute"
-            kind="string"
-            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>
-         <scModule
-               id="de.prob.units.contextAttributeProcessor">
-         </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">
-      </processorType>
-      <processorType
-            class="de.prob.units.sc.ContextAttributeProcessor"
-            id="contextAttributeProcessor"
-            name="contextAttributeProcessor"
-            parent="org.eventb.core.contextModule">
-      </processorType>
-   </extension>
-</plugin>