get errors from prob after unit analysis, only insert the results into the...

get errors from prob after unit analysis, only insert the results into the rodin db if no errors occured

de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java

@@ -45,6 +45,7 @@ import de.prob.core.command.ActivateUnitPluginCommand;
 import de.prob.core.command.ClearMachineCommand;
 import de.prob.core.command.CommandException;
 import de.prob.core.command.ComposedCommand;
+import de.prob.core.command.GetErrorsCommand;
 import de.prob.core.command.GetPluginResultCommand;
 import de.prob.core.command.SetPreferencesCommand;
 import de.prob.core.command.StartAnimationCommand;
@@ -129,15 +130,14 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
 				final ClearMachineCommand clear = new ClearMachineCommand();
 				final SetPreferencesCommand setPrefs = SetPreferencesCommand
 						.createSetPreferencesCommand(animator);
-
 				final InternalLoadCommand load = new InternalLoadCommand(
 						rootElement);
 				final StartAnimationCommand start = new StartAnimationCommand();
-
 				final ActivateUnitPluginCommand activatePlugin = new ActivateUnitPluginCommand();
+				final GetErrorsCommand getErrors = new GetErrorsCommand();
 
 				final ComposedCommand composed = new ComposedCommand(clear,
-						setPrefs, load, start, activatePlugin);
+						setPrefs, load, start, activatePlugin, getErrors);
 
 				animator.execute(composed);
 
@@ -147,27 +147,69 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
 
 				animator.execute(pluginResultCommand);
 
-				ListPrologTerm output = pluginResultCommand.getResult();
-				// System.out.println("Resulting state: " + output);
+				// if no errors occured, insert the results into the rodin
+				// database
+				if (getErrors.getErrors().isEmpty()) {
+					processResults(pluginResultCommand.getResult());
+				} else {
+					// TODO display errors
+				}
+
+				// TODO: should i shutdown the animator?
+				// animator.shutdown();
+			} catch (ProBException e) {
+				e.notifyUserOnce();
+				throw new ExecutionException("Unit Analysis Failed", e);
+			} catch (RodinDBException e) {
+				throw new ExecutionException(
+						"Unit Analysis Failed with a RodinDBException", e);
+			}
+		}
+		return null;
+	}
+
+	private boolean checkErrorMarkers(final IFile resource, List<String> errors) {
+		boolean result = false;
+		IProject project = resource.getProject();
+		try {
+			IMarker[] markers = project.findMarkers(
+					"org.eclipse.core.resources.problemmarker", true,
+					IResource.DEPTH_INFINITE);
+			for (IMarker iMarker : markers) {
+				errors.add(iMarker.getResource().getName()
+						+ ": "
+						+ iMarker
+								.getAttribute(IMarker.MESSAGE, "unknown Error"));
+				result = result
+						|| (Integer) iMarker.getAttribute(IMarker.SEVERITY) == IMarker.SEVERITY_ERROR;
+			}
+
+		} catch (CoreException e1) {
+		}
+		return result;
+	}
 
+	private void processResults(ListPrologTerm result) throws RodinDBException,
+			ExecutionException {
 		// preprocess the list into a map
 		Map<String, String> variables = new HashMap<String, String>();
-				for (PrologTerm term : output) {
+		for (PrologTerm term : result) {
 			CompoundPrologTerm compoundTerm;
 			try {
-						compoundTerm = BindingGenerator.getCompoundTerm(term,
-								"bind", 2);
+				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();
-						throw commandException;
 			}
-					variables.put(PrologTerm.atomicString(compoundTerm
-							.getArgument(1)), PrologTerm
-							.atomicString(compoundTerm.getArgument(2)));
 		}
 
+		IEventBRoot rootElement = getRootElement();
 		// look up the variables / constants of the selected machine in
 		// the state
 		// and set the inferredUnitPragma attribute
@@ -202,43 +244,10 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
 			}
 		} else {
 			throw new ExecutionException(
-							"Cannot translate anything else than IMachineRoot or IContextRoot. Type of "
+					"Cannot execute unit analysis on this element type. Type of "
 							+ rootElement.getComponentName() + " was: "
 							+ rootElement.getClass());
 		}
-
-				// TODO: should i shutdown the animator?
-				// animator.shutdown();
-			} catch (ProBException e) {
-				e.notifyUserOnce();
-				throw new ExecutionException("Unit Analysis Failed", e);
-			} catch (RodinDBException e) {
-				throw new ExecutionException(
-						"Unit Analysis Failed with a RodinDBException", e);
-			}
-		}
-		return null;
-	}
-
-	private boolean checkErrorMarkers(final IFile resource, List<String> errors) {
-		boolean result = false;
-		IProject project = resource.getProject();
-		try {
-			IMarker[] markers = project.findMarkers(
-					"org.eclipse.core.resources.problemmarker", true,
-					IResource.DEPTH_INFINITE);
-			for (IMarker iMarker : markers) {
-				errors.add(iMarker.getResource().getName()
-						+ ": "
-						+ iMarker
-								.getAttribute(IMarker.MESSAGE, "unknown Error"));
-				result = result
-						|| (Integer) iMarker.getAttribute(IMarker.SEVERITY) == IMarker.SEVERITY_ERROR;
-			}
-
-		} catch (CoreException e1) {
-		}
-		return result;
 	}
 
 	private IEventBRoot getRootElement() {