From 5feac5130d699ae35f189bd5e6160299bbfbc7f1 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Fri, 4 Jan 2013 13:43:45 +0100
Subject: [PATCH] animator is shut down by the activation once rodin is quit.
no need to do it here.
---
.../src/de/prob/ui/eventb/StartUnitAnalysisHandler.java | 4 ----
1 file changed, 4 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 909710f2..ad8b1ebf 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
@@ -45,7 +45,6 @@ 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;
@@ -142,9 +141,6 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
animator.execute(pluginResultCommand);
processResults(pluginResultCommand.getResult());
-
- // TODO: should i shutdown the animator?
- // animator.shutdown();
} catch (ProBException e) {
e.notifyUserOnce();
throw new ExecutionException("Unit Analysis Failed", e);
--
GitLab