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 52c57b7a6b4ff598d20fcf139a29fe680fccdc6b..909710f22a1fd5da3dd8b9939d689cd5ea3f08b2 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();