From 5565f05c59591f109a513a150fb5bf10adf2bef5 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Fri, 4 Jan 2013 13:41:54 +0100
Subject: [PATCH] okay, error handling is done in the animator. no need to do
it here.
---
.../de/prob/ui/eventb/StartUnitAnalysisHandler.java | 11 ++---------
1 file changed, 2 insertions(+), 9 deletions(-)
diff --git a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
index 52c57b7a..909710f2 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
@@ -130,10 +130,9 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
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, getErrors);
+ setPrefs, load, start, activatePlugin);
animator.execute(composed);
@@ -142,13 +141,7 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
animator.execute(pluginResultCommand);
- // if no errors occured, insert the results into the rodin
- // database
- if (getErrors.getErrors().isEmpty()) {
- processResults(pluginResultCommand.getResult());
- } else {
- // TODO display errors
- }
+ processResults(pluginResultCommand.getResult());
// TODO: should i shutdown the animator?
// animator.shutdown();
--
GitLab