From c428191a856c489d28eecd26c404a0ae1c5e652e Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Fri, 18 Jan 2013 17:00:45 +0100
Subject: [PATCH] improved error reporting: attach error marker to variables
 with incorrect unit definitions

---
 .../core/command/GetPluginResultCommand.java  | 11 ++-
 .../units/ui/StartUnitAnalysisHandler.java    | 99 ++++++++++++++-----
 2 files changed, 80 insertions(+), 30 deletions(-)

diff --git a/de.prob.core/src/de/prob/core/command/GetPluginResultCommand.java b/de.prob.core/src/de/prob/core/command/GetPluginResultCommand.java
index eb99459f..7e28630b 100644
--- a/de.prob.core/src/de/prob/core/command/GetPluginResultCommand.java
+++ b/de.prob.core/src/de/prob/core/command/GetPluginResultCommand.java
@@ -10,27 +10,29 @@ 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.ListPrologTerm;
+import de.prob.prolog.term.CompoundPrologTerm;
 import de.prob.prolog.term.PrologTerm;
 
 public final class GetPluginResultCommand implements IComposableCommand {
 
 	private final String resultID;
-	private ListPrologTerm result;
+	private CompoundPrologTerm result;
 
 	public GetPluginResultCommand(final String resultID) {
 		this.resultID = resultID;
 	}
 
-	public ListPrologTerm getResult() {
+	public CompoundPrologTerm getResult() {
 		return result;
 	}
 
+	@Override
 	public void processResult(
 			final ISimplifiedROMap<String, PrologTerm> bindings)
 			throws CommandException {
 		try {
-			result = BindingGenerator.getList(bindings, "Bindings");
+			result = BindingGenerator.getCompoundTerm(bindings.get("Bindings"),
+					1);
 		} catch (ResultParserException e) {
 			CommandException commandException = new CommandException(
 					e.getLocalizedMessage(), e);
@@ -39,6 +41,7 @@ public final class GetPluginResultCommand implements IComposableCommand {
 		}
 	}
 
+	@Override
 	public void writeCommand(final IPrologTermOutput pto) {
 		pto.openTerm("get_plugin_output").printAtomOrNumber(resultID)
 				.printVariable("Bindings").closeTerm();
diff --git a/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java b/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java
index dd897bd7..20dffe8c 100644
--- a/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java
+++ b/de.prob.units/src/de/prob/units/ui/StartUnitAnalysisHandler.java
@@ -58,6 +58,7 @@ import de.prob.prolog.term.CompoundPrologTerm;
 import de.prob.prolog.term.ListPrologTerm;
 import de.prob.prolog.term.PrologTerm;
 import de.prob.units.pragmas.InferredUnitPragmaAttribute;
+import de.prob.units.pragmas.UnitPragmaAttribute;
 import de.prob.units.problems.MultipleUnitsInferredMarker;
 
 public class StartUnitAnalysisHandler extends AbstractHandler implements
@@ -75,6 +76,7 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
 			}
 		}
 
+		@Override
 		public void resourceChanged(final IResourceChangeEvent event) {
 			if (path != null) {
 				final IResourceDelta delta = event.getDelta();
@@ -89,6 +91,7 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
 	private ISelection fSelection;
 	private ModificationListener listener;
 
+	@Override
 	public Object execute(final ExecutionEvent event) throws ExecutionException {
 
 		fSelection = HandlerUtil.getCurrentSelection(event);
@@ -134,16 +137,14 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
 				final StartAnimationCommand start = new StartAnimationCommand();
 				final ActivateUnitPluginCommand activatePlugin = new ActivateUnitPluginCommand();
 
-				final ComposedCommand composed = new ComposedCommand(clear,
-						setPrefs, load, start, activatePlugin);
-
-				animator.execute(composed);
-
 				GetPluginResultCommand pluginResultCommand = new GetPluginResultCommand(
 						"Grounded Result State");
 
-				animator.execute(pluginResultCommand);
+				final ComposedCommand composed = new ComposedCommand(clear,
+						setPrefs, load, start, activatePlugin,
+						pluginResultCommand);
 
+				animator.execute(composed);
 				processResults(pluginResultCommand.getResult());
 			} catch (ProBException e) {
 				e.notifyUserOnce();
@@ -194,23 +195,41 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
 		return result;
 	}
 
-	private void processResults(ListPrologTerm result) throws RodinDBException,
-			ExecutionException {
+	private void processResults(CompoundPrologTerm result)
+			throws RodinDBException, ExecutionException {
 		// preprocess the list into a map
 		Map<String, String> variables = new HashMap<String, String>();
-		for (PrologTerm term : result) {
-			CompoundPrologTerm compoundTerm;
-			try {
-				compoundTerm = BindingGenerator
-						.getCompoundTerm(term, "bind", 2);
-
-				variables.put(
-						PrologTerm.atomicString(compoundTerm.getArgument(1)),
-						PrologTerm.atomicString(compoundTerm.getArgument(2)));
-			} catch (ResultParserException e) {
-				CommandException commandException = new CommandException(
-						e.getLocalizedMessage(), e);
-				commandException.notifyUserOnce();
+		List<String> offendingDefinitions = new ArrayList<String>();
+
+		ListPrologTerm liste = BindingGenerator.getList(result.getArgument(1));
+
+		for (PrologTerm term : liste) {
+			if (term.isAtom()) {
+				// this is an error message. do something about it.
+				String offendingUnitDefinition = PrologTerm.atomicString(term)
+						.replace("Incorrect unit definition: ['", "");
+				offendingUnitDefinition = offendingUnitDefinition.replace("']",
+						"");
+
+				// add error to the list of incorrect definitions. error markers
+				// will be attached later
+				offendingDefinitions.add(offendingUnitDefinition);
+
+			} else {
+				// process inferred units and add to map
+				CompoundPrologTerm compoundTerm;
+				try {
+					compoundTerm = BindingGenerator.getCompoundTerm(term,
+							"bind", 2);
+
+					variables.put(PrologTerm.atomicString(compoundTerm
+							.getArgument(1)), PrologTerm
+							.atomicString(compoundTerm.getArgument(2)));
+				} catch (ResultParserException e) {
+					CommandException commandException = new CommandException(
+							e.getLocalizedMessage(), e);
+					commandException.notifyUserOnce();
+				}
 			}
 		}
 
@@ -247,6 +266,20 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
 												+ variableName));
 					}
 				}
+
+				// check if the attached unit pragma (given by user) was marked
+				// as offending
+				if (var.hasAttribute(UnitPragmaAttribute.ATTRIBUTE)) {
+					if (offendingDefinitions.contains(var
+							.getAttributeValue(UnitPragmaAttribute.ATTRIBUTE))) {
+						var.createProblemMarker(
+								InferredUnitPragmaAttribute.ATTRIBUTE,
+								new MultipleUnitsInferredMarker(
+										IMarker.SEVERITY_ERROR,
+										"Incorrect Unit Definition on Variable "
+												+ variableName));
+					}
+				}
 			}
 
 		} else if (rootElement instanceof IContextRoot) {
@@ -254,16 +287,16 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
 			IConstant[] allConstants = rootElement.getContextRoot()
 					.getConstants();
 
-			for (IConstant var : allConstants) {
-				String constantName = var.getIdentifierString();
+			for (IConstant cst : allConstants) {
+				String constantName = cst.getIdentifierString();
 				if (variables.containsKey(constantName)) {
-					var.setAttributeValue(
+					cst.setAttributeValue(
 							InferredUnitPragmaAttribute.ATTRIBUTE,
 							variables.get(constantName),
 							new NullProgressMonitor());
 
 					if (variables.get(constantName).equals("error")) {
-						var.createProblemMarker(
+						cst.createProblemMarker(
 								InferredUnitPragmaAttribute.ATTRIBUTE,
 								new MultipleUnitsInferredMarker(
 										IMarker.SEVERITY_ERROR,
@@ -271,7 +304,7 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
 												+ constantName));
 					}
 					if (variables.get(constantName).equals("unknown")) {
-						var.createProblemMarker(
+						cst.createProblemMarker(
 								InferredUnitPragmaAttribute.ATTRIBUTE,
 								new MultipleUnitsInferredMarker(
 										IMarker.SEVERITY_WARNING,
@@ -279,6 +312,20 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
 												+ constantName));
 					}
 				}
+
+				// check if the attached unit pragma (given by user) was marked
+				// as offending
+				if (cst.hasAttribute(UnitPragmaAttribute.ATTRIBUTE)) {
+					if (offendingDefinitions.contains(cst
+							.getAttributeValue(UnitPragmaAttribute.ATTRIBUTE))) {
+						cst.createProblemMarker(
+								InferredUnitPragmaAttribute.ATTRIBUTE,
+								new MultipleUnitsInferredMarker(
+										IMarker.SEVERITY_ERROR,
+										"Incorrect Unit Definition on Constant "
+												+ constantName));
+					}
+				}
 			}
 		} else {
 			throw new ExecutionException(
-- 
GitLab