package de.prob.ui.eventb;

import java.util.HashMap;

import org.eclipse.core.commands.AbstractHandler;
import org.eclipse.core.commands.ExecutionEvent;
import org.eclipse.core.commands.ExecutionException;
import org.eclipse.core.resources.IFile;
import org.eclipse.jface.viewers.ISelection;
import org.eclipse.jface.viewers.IStructuredSelection;
import org.eclipse.ui.handlers.HandlerUtil;
import org.eventb.core.IEventBRoot;
import org.rodinp.core.IRodinFile;
import org.rodinp.core.RodinCore;

import com.google.inject.Injector;

import de.prob.Main;
import de.prob.model.eventb.EventBModel;
import de.prob.scripting.Api;
import de.prob.scripting.EventBFactory;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.StateSpace;
import de.prob.statespace.Trace;

public class StartAnimationHandler extends AbstractHandler {

	private ISelection fSelection;

	@Override
	public Object execute(final ExecutionEvent event) throws ExecutionException {

		fSelection = HandlerUtil.getCurrentSelection(event);

		final IEventBRoot rootElement = getRootElement();

		String fileName = rootElement.getResource().getRawLocation()
				.makeAbsolute().toOSString();
		if (fileName.endsWith(".buc")) {
			fileName = fileName.replace(".buc", ".bcc");
		} else {
			fileName = fileName.replace(".bum", ".bcm");
		}

		Injector injector = Main.getInjector();

		final EventBFactory instance = injector
				.getInstance(EventBFactory.class);

		EventBModel model = instance.load(fileName,
				new HashMap<String, String>(), Api.getDEFAULT());

		StateSpace s = model.getStateSpace();

		Trace h = new Trace(s);
		AnimationSelector selector = injector
				.getInstance(AnimationSelector.class);
		selector.addNewAnimation(h);

		System.gc();

		return null;
	}

	private IEventBRoot getRootElement() {
		IEventBRoot root = null;
		if (fSelection instanceof IStructuredSelection) {
			final IStructuredSelection ssel = (IStructuredSelection) fSelection;
			if (ssel.size() == 1) {
				final Object element = ssel.getFirstElement();
				if (element instanceof IEventBRoot) {
					root = (IEventBRoot) element;
				} else if (element instanceof IFile) {
					IRodinFile rodinFile = RodinCore.valueOf((IFile) element);
					if (rodinFile != null) {
						root = (IEventBRoot) rodinFile.getRoot();
					}
				}
			}
		}
		return root;
	}

}

@@ -333,32 +333,234 @@
 turedSelection;%0A
+import org.eclipse.swt.widgets.Display;%0Aimport org.eclipse.ui.IPerspectiveDescriptor;%0Aimport org.eclipse.ui.IWorkbenchWindow;%0Aimport org.eclipse.ui.PlatformUI;%0Aimport org.eclipse.ui.WorkbenchException;%0A
 import org.eclip
@@ -1941,16 +1941,486 @@
 .gc();%0A%0A
+%09%09final IWorkbenchWindow workbenchWindow = PlatformUI.getWorkbench()%0A%09%09%09%09.getActiveWorkbenchWindow();%0A%09%09IPerspectiveDescriptor activePerspective = workbenchWindow%0A%09%09%09%09.getActivePage().getPerspective();%0A%0A%09%09Display.getCurrent().asyncExec(new Runnable() %7B%0A%09%09%09public void run() %7B%0A%09%09%09%09// switch perspective%0A%09%09%09%09try %7B%0A%09%09%09%09%09workbenchWindow.getWorkbench().showPerspective(%0A%09%09%09%09%09%09%09%22de.prob2.perspective%22, workbenchWindow);%0A%09%09%09%09%7D catch (WorkbenchException e) %7B%0A%0A%09%09%09%09%7D%0A%09%09%09%7D%0A%09%09%7D);%0A%0A
 %09%09return

switch perspective