package org.lamport.tla.toolbox.ui.handler;

import org.eclipse.core.commands.AbstractHandler;
import org.eclipse.core.commands.ExecutionEvent;
import org.eclipse.core.commands.ExecutionException;
import org.eclipse.core.commands.IHandler;
import org.eclipse.core.runtime.CoreException;
import org.eclipse.core.runtime.QualifiedName;
import org.lamport.tla.toolbox.Activator;
import org.lamport.tla.toolbox.ui.perspective.InitialPerspective;
import org.lamport.tla.toolbox.ui.view.ProblemView;
import org.lamport.tla.toolbox.util.UIHelper;

/**
 * Closes the specification and switches the UI back to the initial perspective
 *
 * @author zambrovski
 */
public class CloseSpecHandler extends AbstractHandler implements IHandler
{
    public final static String COMMAND_ID = "toolbox.command.spec.close";
    
    // A QualifiedName for the project's last closed time persistent property.
    public static final QualifiedName LAST_CLOSED_DATE = 
        new QualifiedName(COMMAND_ID, "lastClosedTime");

    public Object execute(ExecutionEvent event) throws ExecutionException
    {
        // Set the project's last closed time to the current time.
        try
        {
            Activator.getSpecManager().getSpecLoaded().getProject().setPersistentProperty(
               LAST_CLOSED_DATE, "" + System.currentTimeMillis());
        } catch (CoreException e)
        {
            // TODO Auto-generated catch block
            Activator.getDefault().logDebug(
             "Exception thrown when setting project LAST_CLOSED time.");
        }
        // close all editors
        UIHelper.getActivePage().closeAllEditors(true);
        // hide errors
        UIHelper.hideView(ProblemView.ID);
        // switch perspective
        UIHelper.switchPerspective(InitialPerspective.ID);
        // unset the spec
        Activator.getSpecManager().setSpecLoaded(null);
        return null;
    }

	/* (non-Javadoc)
	 * @see org.eclipse.core.commands.AbstractHandler#isEnabled()
	 */
	@Override
	public boolean isEnabled() {
		if (Activator.getSpecManager().getSpecLoaded() == null) {
			return false;
		}
		return super.isEnabled();
	}

}

@@ -374,24 +374,196 @@
 Activator;%0D%0A
+import org.lamport.tla.toolbox.spec.Spec;%0D%0Aimport org.lamport.tla.toolbox.spec.manager.WorkspaceSpecManager;%0D%0Aimport org.lamport.tla.toolbox.ui.navigator.ToolboxExplorer;%0D%0A
 import org.l
@@ -2012,61 +2012,632 @@
     
-// unset the spec%0D%0A        Activator.getSpecManager()
+%0D%0A        // Refresh the CommonViewer to causes it to align the icon shown in the SpecExplorer%0D%0A        // with the state of the spec. E.g. if the spec is closed, make sure it shows the closed%0D%0A        // project icon.%0D%0A        final WorkspaceSpecManager specManager = Activator.getSpecManager();%0D%0A        final ToolboxExplorer toolboxExplorer = (ToolboxExplorer) UIHelper.findView(ToolboxExplorer.VIEW_ID);%0D%0A        if (toolboxExplorer != null) %7B%0D%0A%09%09%09final Spec specClosed = specManager.getSpecLoaded();%0D%0A%09%09%09toolboxExplorer.getCommonViewer().refresh(specClosed);%0D%0A        %7D%0D%0A%0D%0A        // unset the spec%0D%0A        specManager
 .set
@@ -2775,16 +2775,18 @@
 %0D%0A%09 */%0D%0A
+//
 %09@Overri
@@ -2789,16 +2789,18 @@
 erride%0D%0A
+//
 %09public 
@@ -2822,16 +2822,18 @@
 ed() %7B%0D%0A
+//
 %09%09if (Ac
@@ -2885,16 +2885,18 @@
 ull) %7B%0D%0A
+//
 %09%09%09retur
@@ -2909,13 +2909,17 @@
 e;%0D%0A
+//
 %09%09%7D%0D%0A
+//
 %09%09re
@@ -2943,16 +2943,18 @@
 led();%0D%0A
+//
 %09%7D%0D%0A%0D%0A%7D%0D

Refresh the CommonViewer embedded in the ToolboxExplorer to causes it to align the icon shown in the SpecExplorer with the actual state of the spec. E.g. if the spec is closed, make sure it shows the closed project icon.