Skip to content
Snippets Groups Projects
Commit 37dfaff1 authored by Markus Alexander Kuppe's avatar Markus Alexander Kuppe
Browse files

Toolbox launch fails during tests.

The Toolbox initialization can be described as hackery with layers of workaround on top. This has finally proven unmaintainable which caused this larger refactoring.

It now checks the instance location at the correct place instead of in the Activator. Formerly it was done in the Activator, because it would run before the Application which was a result of an upside-down extension point. With the extension point reversed, the Application is executed prior to the Activator.

[Bug](Toolbox]
parent 80943d84
No related branches found
No related tags found
No related merge requests found
Showing
with 373 additions and 185 deletions
...@@ -13,7 +13,8 @@ Require-Bundle: org.eclipse.ui, ...@@ -13,7 +13,8 @@ Require-Bundle: org.eclipse.ui,
org.eclipse.ui.forms, org.eclipse.ui.forms,
org.eclipse.ui.ide;bundle-version="3.4.1", org.eclipse.ui.ide;bundle-version="3.4.1",
org.eclipse.swt, org.eclipse.swt,
org.lamport.tla.toolbox;bundle-version="1.0.0",
org.eclipse.equinox.p2.ui.sdk.scheduler;bundle-version="1.0.0" org.eclipse.equinox.p2.ui.sdk.scheduler;bundle-version="1.0.0"
Bundle-ActivationPolicy: lazy Bundle-ActivationPolicy: lazy
Bundle-Activator: org.lamport.tla.toolbox.StandaloneActivator Bundle-Activator: org.lamport.tla.toolbox.StandaloneActivator
Export-Package: org.lamport.tla.toolbox.lifecycle,
org.lamport.tla.toolbox.ui.intro
org.lamport.tla.toolbox.product.standalone/images/splash_small.bmp

120 KiB

<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<?eclipse version="3.2"?> <?eclipse version="3.2"?>
<plugin> <plugin>
<extension-point id="org.lamport.tla.toolbox.tool" name="Toolbox Life Cycle Participant" schema="schema/org.lamport.tla.toolbox.tool.exsd"/>
<!-- --> <!-- -->
<!-- Application --> <!-- Application -->
...@@ -48,7 +49,7 @@ ...@@ -48,7 +49,7 @@
<extension <extension
point="org.eclipse.ui.intro"> point="org.eclipse.ui.intro">
<intro <intro
class="org.lamport.tla.toolbox.ui.intro.ToolboxIntoPart" class="org.lamport.tla.toolbox.ui.intro.ToolboxIntroPart"
id="org.lamport.tla.toolbox.product.standalone.intro"> id="org.lamport.tla.toolbox.product.standalone.intro">
</intro> </intro>
<introProductBinding <introProductBinding
......
// Copyright (c) Jan 30, 2012 Microsoft Corporation. All rights reserved. // Copyright (c) Jan 30, 2012 Microsoft Corporation. All rights reserved.
package org.lamport.tla.toolbox; package org.lamport.tla.toolbox;
import java.io.File;
import java.io.IOException;
import org.eclipse.core.runtime.Platform;
import org.eclipse.equinox.app.IApplication; import org.eclipse.equinox.app.IApplication;
import org.eclipse.equinox.app.IApplicationContext; import org.eclipse.equinox.app.IApplicationContext;
import org.eclipse.jface.dialogs.MessageDialog;
import org.eclipse.osgi.service.datalocation.Location;
import org.eclipse.osgi.util.NLS;
import org.eclipse.swt.widgets.Display; import org.eclipse.swt.widgets.Display;
import org.eclipse.ui.IWorkbench; import org.eclipse.ui.IWorkbench;
import org.eclipse.ui.PlatformUI; import org.eclipse.ui.PlatformUI;
...@@ -11,7 +18,6 @@ import org.eclipse.ui.PlatformUI; ...@@ -11,7 +18,6 @@ import org.eclipse.ui.PlatformUI;
* This class controls all aspects of the application's execution * This class controls all aspects of the application's execution
* *
* @author Simon Zambrovski * @author Simon Zambrovski
* @version $Id$
*/ */
public class Application implements IApplication { public class Application implements IApplication {
...@@ -36,6 +42,36 @@ public class Application implements IApplication { ...@@ -36,6 +42,36 @@ public class Application implements IApplication {
} }
} }
// The call to getStateLocation makes sure the instance location gets
// initialized before we call .lock on it.
StandaloneActivator.getDefault().getStateLocation();
final Location instanceLocation = Platform.getInstanceLocation();
// Only allow a single Toolbox instance per workspace to prevent data
// corruption in the workspace files.
try {
if (!instanceLocation.lock()) {
final File workspaceDirectory = new File(Platform.getInstanceLocation().getURL().getFile());
if (workspaceDirectory.exists()) {
MessageDialog.openError(PlatformUI.createDisplay().getActiveShell(), "Toolbox files cannot be locked",
NLS.bind(
"Could not launch the Toolbox because the associated workspace is currently in use by another Toolbox. Opening two instances on the same workspace leads to data corruption.\n\n"
+ "If this is incorrect and there is no other Toolbox running, an earlier Toolbox terminated without releasing the lock. Please manually delete the lock file ''{0}'' and try restarting the Toolbox.",
workspaceDirectory.getAbsolutePath()
.concat(File.separator + ".metadata" + File.separator + ".lock")));
}
// We showed an error to the user, lets do a "clean" (0) exit to
// not raise a second window with a detailed technical error.
System.exit(0);
}
} catch (IOException e) {
StandaloneActivator.getDefault().logError("Toolbox files cannot be locked", e);
MessageDialog.openError(PlatformUI.createDisplay().getActiveShell(), "Toolbox files cannot be locked",
"Could not launch the Toolbox because acquiring the associated workspace lock failed. We are sorry, this is a bug. Please get in contact with us.");
// We showed an error to the user, lets do a "clean" (0) exit to
// not raise a second window with a detailed technical error.
System.exit(0);
}
Display display = PlatformUI.createDisplay(); Display display = PlatformUI.createDisplay();
try { try {
int returnCode = PlatformUI.createAndRunWorkbench(display, int returnCode = PlatformUI.createAndRunWorkbench(display,
......
...@@ -9,24 +9,18 @@ import org.eclipse.ui.application.IWorkbenchWindowConfigurer; ...@@ -9,24 +9,18 @@ import org.eclipse.ui.application.IWorkbenchWindowConfigurer;
import org.eclipse.ui.application.WorkbenchAdvisor; import org.eclipse.ui.application.WorkbenchAdvisor;
import org.eclipse.ui.application.WorkbenchWindowAdvisor; import org.eclipse.ui.application.WorkbenchWindowAdvisor;
import org.eclipse.ui.ide.IDE; import org.eclipse.ui.ide.IDE;
import org.lamport.tla.toolbox.tool.ToolboxHandle; import org.lamport.tla.toolbox.ui.intro.ToolboxIntroPart;
import org.lamport.tla.toolbox.tool.ToolboxLifecycleException;
import org.lamport.tla.toolbox.tool.ToolboxLifecycleParticipant;
import org.lamport.tla.toolbox.util.ToolboxLifecycleParticipantManger;
import org.lamport.tla.toolbox.util.UIHelper;
import org.osgi.framework.Bundle; import org.osgi.framework.Bundle;
/** /**
* This workbench advisor creates the window advisor, and specifies * This workbench advisor creates the window advisor, and specifies
* the perspective id for the initial window. * the perspective id for the initial window.
* @author Simon Zambrovski * @author Simon Zambrovski
* @version $Id$
*/ */
public class ApplicationWorkbenchAdvisor extends WorkbenchAdvisor public class ApplicationWorkbenchAdvisor extends WorkbenchAdvisor
{ {
// TODO MOVE! // TODO MOVE!
public static final String PERSPECTIVE_ID = "org.lamport.tla.toolbox.ui.perspective.initial";
public static final String IDE_PLUGIN = "org.eclipse.ui.ide"; public static final String IDE_PLUGIN = "org.eclipse.ui.ide";
public static final String PATH_OBJECT = "icons/full/obj16/"; public static final String PATH_OBJECT = "icons/full/obj16/";
public static final String PATH_WIZBAN = "icons/full/wizban/"; public static final String PATH_WIZBAN = "icons/full/wizban/";
...@@ -39,7 +33,6 @@ public class ApplicationWorkbenchAdvisor extends WorkbenchAdvisor ...@@ -39,7 +33,6 @@ public class ApplicationWorkbenchAdvisor extends WorkbenchAdvisor
* Image definition from org.eclipse.ui.internal.ide.IDEInternalWorkbenchImages#IMG_DLGBAN_SAVEAS_DLG * Image definition from org.eclipse.ui.internal.ide.IDEInternalWorkbenchImages#IMG_DLGBAN_SAVEAS_DLG
*/ */
public static final String IMG_DLGBAN_SAVEAS_DLG = "IMG_DLGBAN_SAVEAS_DLG"; public static final String IMG_DLGBAN_SAVEAS_DLG = "IMG_DLGBAN_SAVEAS_DLG";
private ToolboxLifecycleParticipant[] registeredTools;
public WorkbenchWindowAdvisor createWorkbenchWindowAdvisor(IWorkbenchWindowConfigurer configurer) public WorkbenchWindowAdvisor createWorkbenchWindowAdvisor(IWorkbenchWindowConfigurer configurer)
{ {
...@@ -48,7 +41,7 @@ public class ApplicationWorkbenchAdvisor extends WorkbenchAdvisor ...@@ -48,7 +41,7 @@ public class ApplicationWorkbenchAdvisor extends WorkbenchAdvisor
public String getInitialWindowPerspectiveId() public String getInitialWindowPerspectiveId()
{ {
return PERSPECTIVE_ID; return ToolboxIntroPart.PERSPECTIVE_ID;
} }
/* /*
...@@ -80,41 +73,19 @@ public class ApplicationWorkbenchAdvisor extends WorkbenchAdvisor ...@@ -80,41 +73,19 @@ public class ApplicationWorkbenchAdvisor extends WorkbenchAdvisor
configurer.declareImage(symbolicName, desc, shared); configurer.declareImage(symbolicName, desc, shared);
} }
public boolean preShutdown() /* (non-Javadoc)
{ * @see org.eclipse.ui.application.WorkbenchAdvisor#preShutdown()
if (!ToolboxHandle.getInstanceStore().getBoolean(ToolboxHandle.I_RESTORE_LAST_SPEC)) */
{ public boolean preShutdown() {
UIHelper.getActivePage().closeAllEditors(true); ToolboxLifecycleParticipantManger.terminate();
UIHelper.switchPerspective(getInitialWindowPerspectiveId());
}
try
{
ToolboxLifecycleParticipantManger.terminate(registeredTools);
} catch (ToolboxLifecycleException e)
{
// TODO
e.printStackTrace();
}
return super.preShutdown(); return super.preShutdown();
} }
public void postStartup() /* (non-Javadoc)
{ * @see org.eclipse.ui.application.WorkbenchAdvisor#postStartup()
*/
public void postStartup() {
super.postStartup(); super.postStartup();
ToolboxLifecycleParticipantManger.initialize();
try
{
registeredTools = ToolboxLifecycleParticipantManger.getRegisteredTools();
ToolboxLifecycleParticipantManger.initialize(registeredTools);
} catch (ToolboxLifecycleException e)
{
// TODO
e.printStackTrace();
} }
}
} }
...@@ -15,8 +15,6 @@ import org.eclipse.ui.application.IActionBarConfigurer; ...@@ -15,8 +15,6 @@ import org.eclipse.ui.application.IActionBarConfigurer;
import org.eclipse.ui.application.IWorkbenchWindowConfigurer; import org.eclipse.ui.application.IWorkbenchWindowConfigurer;
import org.eclipse.ui.application.WorkbenchWindowAdvisor; import org.eclipse.ui.application.WorkbenchWindowAdvisor;
import org.eclipse.ui.internal.ide.EditorAreaDropAdapter; import org.eclipse.ui.internal.ide.EditorAreaDropAdapter;
import org.lamport.tla.toolbox.ui.navigator.ToolboxExplorer;
import org.lamport.tla.toolbox.ui.view.ProblemView;
/** /**
* Configuration of the main window * Configuration of the main window
...@@ -85,14 +83,11 @@ public class ApplicationWorkbenchWindowAdvisor extends WorkbenchWindowAdvisor ...@@ -85,14 +83,11 @@ public class ApplicationWorkbenchWindowAdvisor extends WorkbenchWindowAdvisor
} }
} }
} }
super.postWindowOpen();
// At this point in time we can be certain that the UI is fully // At this point in time we can be certain that the UI is fully
// instantiated (views, editors, menus...). Thus, register // instantiated (views, editors, menus...). Thus, register
// listeners that connect the UI to the workspace resources. // listeners that connect the UI to the workspace resources.
ProblemView.ResourceListener.init(); ToolboxLifecycleParticipantManger.postWorkbenchWindowOpen();
ToolboxExplorer.ResourceListener.init();
super.postWindowOpen();
} }
} }
...@@ -2,16 +2,20 @@ ...@@ -2,16 +2,20 @@
package org.lamport.tla.toolbox; package org.lamport.tla.toolbox;
import org.eclipse.core.runtime.IStatus;
import org.eclipse.core.runtime.Status;
import org.eclipse.ui.plugin.AbstractUIPlugin;
/** /**
* @author Markus Alexander Kuppe * @author Markus Alexander Kuppe
*/ */
public class StandaloneActivator extends AbstractTLCActivator { public class StandaloneActivator extends AbstractUIPlugin {
private static final int DEBUG_SEVERITY = -1;
public static final String PLUGIN_ID = "org.lamport.tla.toolbox.product.standalone"; public static final String PLUGIN_ID = "org.lamport.tla.toolbox.product.standalone";
private static StandaloneActivator plugin; private static StandaloneActivator plugin;
public StandaloneActivator() { public StandaloneActivator() {
super(PLUGIN_ID);
plugin = this; plugin = this;
} }
...@@ -23,4 +27,64 @@ public class StandaloneActivator extends AbstractTLCActivator { ...@@ -23,4 +27,64 @@ public class StandaloneActivator extends AbstractTLCActivator {
public static StandaloneActivator getDefault() { public static StandaloneActivator getDefault() {
return plugin; return plugin;
} }
/**
* Writes a string and a cause into the error category of the log
*
* @param string
*/
public void logError(String message) {
getLog().log(new Status(IStatus.ERROR, PLUGIN_ID, message));
}
/**
* Writes a string and a cause into the error category of the log
*
* @param string
* @param e
*/
public void logError(String message, Throwable cause) {
getLog().log(new Status(IStatus.ERROR, PLUGIN_ID, message, cause));
}
/**
* Writes a string and a cause into the warning category of the log
*
* @param string
*/
public void logWarning(String message) {
getLog().log(new Status(IStatus.WARNING, PLUGIN_ID, message));
}
/**
* Writes a string and a cause into the warning category of the log
*
* @param string
*/
public void logWarning(String message, Throwable cause) {
getLog().log(new Status(IStatus.WARNING, PLUGIN_ID, message, cause));
}
/**
* Writes a string into some debugging place
*/
public void logDebug(String message) {
logDebug(message, null);
}
/**
* Writes a string into some debugging place
*/
public void logDebug(String message, Throwable cause) {
getLog().log(new Status(IStatus.INFO, PLUGIN_ID, DEBUG_SEVERITY, message, cause));
}
/**
* Writes a string into the info category of the log
*
* @param string
*/
public void logInfo(String message) {
getLog().log(new Status(IStatus.INFO, PLUGIN_ID, message));
}
} }
package org.lamport.tla.toolbox.util; package org.lamport.tla.toolbox;
import org.eclipse.core.runtime.Assert; import org.eclipse.core.runtime.Assert;
import org.eclipse.core.runtime.CoreException; import org.eclipse.core.runtime.CoreException;
import org.eclipse.core.runtime.IConfigurationElement; import org.eclipse.core.runtime.IConfigurationElement;
import org.eclipse.core.runtime.Platform; import org.eclipse.core.runtime.Platform;
import org.lamport.tla.toolbox.tool.ToolboxLifecycleException; import org.lamport.tla.toolbox.lifecycle.ToolboxLifecycleParticipant;
import org.lamport.tla.toolbox.tool.ToolboxLifecycleParticipant;
/** /**
* Provides methods for accessing the extensions registered to the toolbox extension points * Provides methods for accessing the extensions registered to the toolbox extension points
* *
* @author Simon Zambrovski * @author Simon Zambrovski
* @version $Id$
*/ */
public class ToolboxLifecycleParticipantManger public class ToolboxLifecycleParticipantManger
{ {
...@@ -22,7 +20,7 @@ public class ToolboxLifecycleParticipantManger ...@@ -22,7 +20,7 @@ public class ToolboxLifecycleParticipantManger
* Retrieves tools registered * Retrieves tools registered
* @return * @return
*/ */
public static ToolboxLifecycleParticipant[] getRegisteredTools() throws ToolboxLifecycleException private static ToolboxLifecycleParticipant[] getRegisteredTools()
{ {
IConfigurationElement[] decls = Platform.getExtensionRegistry().getConfigurationElementsFor(POINT); IConfigurationElement[] decls = Platform.getExtensionRegistry().getConfigurationElementsFor(POINT);
ToolboxLifecycleParticipant[] extensions = new ToolboxLifecycleParticipant[decls.length]; ToolboxLifecycleParticipant[] extensions = new ToolboxLifecycleParticipant[decls.length];
...@@ -34,7 +32,8 @@ public class ToolboxLifecycleParticipantManger ...@@ -34,7 +32,8 @@ public class ToolboxLifecycleParticipantManger
extensions[i] = (ToolboxLifecycleParticipant) decls[i].createExecutableExtension(CLASS_ATTR_NAME); extensions[i] = (ToolboxLifecycleParticipant) decls[i].createExecutableExtension(CLASS_ATTR_NAME);
} catch (CoreException e) } catch (CoreException e)
{ {
throw new ToolboxLifecycleException("Error retrieving the registered tools", e); StandaloneActivator.getDefault().logError(e.getMessage(), e);
return new ToolboxLifecycleParticipant[0];
} }
} }
return extensions; return extensions;
...@@ -43,10 +42,10 @@ public class ToolboxLifecycleParticipantManger ...@@ -43,10 +42,10 @@ public class ToolboxLifecycleParticipantManger
/** /**
* Distributes the initialize message * Distributes the initialize message
* @param participants * @param participants
* @throws ToolboxLifecycleException
*/ */
public static void initialize(ToolboxLifecycleParticipant[] participants) throws ToolboxLifecycleException public static void initialize()
{ {
final ToolboxLifecycleParticipant[] participants = getRegisteredTools();
Assert.isNotNull(participants); Assert.isNotNull(participants);
// Activator.getDefault().logDebug("Initializing the tools"); // Activator.getDefault().logDebug("Initializing the tools");
for (int i = 0; i < participants.length; i++) for (int i = 0; i < participants.length; i++)
...@@ -55,13 +54,21 @@ public class ToolboxLifecycleParticipantManger ...@@ -55,13 +54,21 @@ public class ToolboxLifecycleParticipantManger
} }
} }
public static void postWorkbenchWindowOpen() {
final ToolboxLifecycleParticipant[] participants = getRegisteredTools();
Assert.isNotNull(participants);
for (int i = 0; i < participants.length; i++) {
participants[i].postWorkbenchWindowOpen();
}
}
/** /**
* Distributes the terminate message * Distributes the terminate message
* @param participants * @param participants
* @throws ToolboxLifecycleException
*/ */
public static void terminate(ToolboxLifecycleParticipant[] participants) throws ToolboxLifecycleException public static void terminate()
{ {
final ToolboxLifecycleParticipant[] participants = getRegisteredTools();
Assert.isNotNull(participants); Assert.isNotNull(participants);
// Activator.getDefault().logDebug("Terminating the tools"); // Activator.getDefault().logDebug("Terminating the tools");
for (int i = 0; i < participants.length; i++) for (int i = 0; i < participants.length; i++)
...@@ -69,5 +76,4 @@ public class ToolboxLifecycleParticipantManger ...@@ -69,5 +76,4 @@ public class ToolboxLifecycleParticipantManger
participants[i].terminate(); participants[i].terminate();
} }
} }
} }
package org.lamport.tla.toolbox.tool; package org.lamport.tla.toolbox.lifecycle;
import org.eclipse.ui.IWorkbenchWindow;
/** /**
* Describes a basic interface for the tool contribution * Describes a basic interface for the tool contribution
* *
* @author Simon Zambrovski * @author Simon Zambrovski
* @version $Id$
*/ */
public abstract class ToolboxLifecycleParticipant public abstract class ToolboxLifecycleParticipant
{ {
/** /**
* Is called during toolbox initialization * Is called during toolbox initialization
* The implementation is empty, subclasses may override * The implementation is empty, subclasses may override
* @throws ToolboxLifecycleException
*/ */
public void initialize() throws ToolboxLifecycleException public void initialize() {
{ // subclasses may override
}
/**
* Is called when the {@link IWorkbenchWindow} has been opened.
*/
public void postWorkbenchWindowOpen() {
// subclasses may override
} }
/** /**
* Is called during termination of the toolbox. * Is called during termination of the toolbox.
* The implementation is empty, subclasses may override * The implementation is empty, subclasses may override
*
* @throws ToolboxLifecycleException
*/ */
public void terminate() throws ToolboxLifecycleException public void terminate(){
{ // subclasses may override
} }
} }
/*******************************************************************************
* Copyright (c) 2015 Microsoft Research. All rights reserved.
*
* The MIT License (MIT)
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
* of the Software, and to permit persons to whom the Software is furnished to do
* so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
* AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
* WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*
* Contributors:
* Markus Alexander Kuppe - initial API and implementation
******************************************************************************/
package org.lamport.tla.toolbox.ui.intro;
import java.net.URL;
import org.eclipse.core.runtime.FileLocator;
import org.eclipse.core.runtime.Path;
import org.eclipse.jface.resource.ColorDescriptor;
import org.eclipse.jface.resource.FontDescriptor;
import org.eclipse.jface.resource.ImageDescriptor;
import org.eclipse.jface.resource.JFaceResources;
import org.eclipse.jface.resource.LocalResourceManager;
import org.eclipse.swt.SWT;
import org.eclipse.swt.custom.StyleRange;
import org.eclipse.swt.custom.StyledText;
import org.eclipse.swt.graphics.Color;
import org.eclipse.swt.graphics.FontData;
import org.eclipse.swt.graphics.RGB;
import org.eclipse.swt.layout.GridData;
import org.eclipse.swt.layout.GridLayout;
import org.eclipse.swt.widgets.Composite;
import org.eclipse.swt.widgets.Event;
import org.eclipse.swt.widgets.Label;
import org.eclipse.swt.widgets.Listener;
import org.eclipse.ui.PlatformUI;
import org.eclipse.ui.help.IWorkbenchHelpSystem;
import org.eclipse.ui.intro.IIntroPart;
import org.eclipse.ui.part.IntroPart;
import org.osgi.framework.Bundle;
import org.osgi.framework.FrameworkUtil;
public class ToolboxIntroPart extends IntroPart implements IIntroPart {
public static final String PERSPECTIVE_ID = "org.lamport.tla.toolbox.ui.perspective.initial";
private Composite container;
/**
* @wbp.parser.entryPoint
*/
public void createPartControl(Composite container) {
this.container = container;
createControl(container);
}
public static void createControl(Composite container) {
Composite outerContainer = new Composite(container, SWT.NONE);
// The local resource manager takes care of disposing images, fonts and
// colors when
// the outerContainer Composite is disposed.
final LocalResourceManager localResourceManager = new LocalResourceManager(JFaceResources.getResources(),
outerContainer);
final GridLayout gridLayout = new GridLayout();
gridLayout.numColumns = 2;
outerContainer.setLayout(gridLayout);
final Color backgroundColor = localResourceManager
.createColor(ColorDescriptor.createFrom(new RGB(255, 255, 228)));
outerContainer.setBackground(backgroundColor);
/* Logo */
final Label lblImage = new Label(outerContainer, SWT.NONE);
lblImage.setText("Invisible text");
final Bundle bundle = FrameworkUtil.getBundle(ToolboxIntroPart.class);
final URL url = FileLocator.find(bundle, new Path("images/splash_small.bmp"), null);
final ImageDescriptor logoImage = ImageDescriptor.createFromURL(url);
lblImage.setImage(localResourceManager.createImage(logoImage));
/* Welcome header */
final Label lblHeader = new Label(outerContainer, SWT.WRAP);
// Double its font size
final FontDescriptor headerFontDescriptor = JFaceResources.getHeaderFontDescriptor();
final FontData fontData = headerFontDescriptor.getFontData()[0];
lblHeader.setFont(localResourceManager.createFont(headerFontDescriptor.setHeight(fontData.getHeight() * 2)));
// Color value (taken from old style.css)
lblHeader.setForeground(localResourceManager.createColor(new RGB(0, 0, 192)));
lblHeader.setLayoutData(new GridData(SWT.LEFT, SWT.BOTTOM, true, false, 1, 1));
lblHeader.setText("Welcome to the TLA\u207A Toolbox");
lblHeader.setBackground(backgroundColor);
/* What is next section */
Label lblSeparator = new Label(outerContainer, SWT.NONE);
lblSeparator.setLayoutData(new GridData(SWT.LEFT, SWT.CENTER, false, false, 2, 1));
final StyledText styledWhatIsNext = new StyledText(outerContainer, SWT.WRAP | SWT.CENTER);
styledWhatIsNext.setBackground(backgroundColor);
final String whatIsnext = "There is no specification open. Click on Help if you're not sure what you should do next.";
styledWhatIsNext.setText(whatIsnext);
GridData gd_styledWhatIsNext = new GridData(GridData.FILL_HORIZONTAL);
gd_styledWhatIsNext.horizontalAlignment = SWT.LEFT;
gd_styledWhatIsNext.horizontalSpan = 2;
styledWhatIsNext.setLayoutData(gd_styledWhatIsNext);
StyleRange winStyle = new StyleRange();
winStyle.underline = true;
winStyle.underlineStyle = SWT.UNDERLINE_LINK;
int[] winRange = { whatIsnext.indexOf("Help"), "Help".length() };
StyleRange[] winStyles = { winStyle };
styledWhatIsNext.setStyleRanges(winRange, winStyles);
// link styled text to getting started guide
styledWhatIsNext.addListener(SWT.MouseDown, new Listener() {
public void handleEvent(Event event) {
IWorkbenchHelpSystem helpSystem = PlatformUI.getWorkbench().getHelpSystem();
helpSystem.displayHelpResource("/org.lamport.tla.toolbox.doc/html/contents.html");
}
});
/* Getting started text */
final StyledText styledGettingStarted = new StyledText(outerContainer, SWT.WRAP | SWT.CENTER);
styledGettingStarted.setBackground(backgroundColor);
final String lblString = "If this is the first time you have used the Toolbox, please read the Getting Started guide.";
styledGettingStarted.setText(lblString);
GridData gd_styledGettingStarted = new GridData(GridData.FILL_HORIZONTAL);
gd_styledGettingStarted.horizontalAlignment = SWT.LEFT;
gd_styledGettingStarted.horizontalSpan = 2;
styledGettingStarted.setLayoutData(gd_styledGettingStarted);
new Label(outerContainer, SWT.NONE);
new Label(outerContainer, SWT.NONE);
StyleRange style = new StyleRange();
style.underline = true;
style.underlineStyle = SWT.UNDERLINE_LINK;
int[] range = { lblString.indexOf("Getting Started"), "Getting Started".length() };
StyleRange[] styles = { style };
styledGettingStarted.setStyleRanges(range, styles);
// link styled text to getting started guide
styledGettingStarted.addListener(SWT.MouseDown, new Listener() {
public void handleEvent(Event event) {
IWorkbenchHelpSystem helpSystem = PlatformUI.getWorkbench().getHelpSystem();
helpSystem.displayHelpResource("/org.lamport.tla.toolbox.doc/html/gettingstarted/gettingstarted.html");
}
});
/* Toolbox version */
final Label verticalFillUp = new Label(outerContainer, SWT.NONE);
verticalFillUp.setLayoutData(new GridData(SWT.FILL, SWT.CENTER, false, true, 2, 1));
verticalFillUp.setBackground(backgroundColor);
final Label horizontalLine = new Label(outerContainer, SWT.SEPARATOR | SWT.HORIZONTAL);
horizontalLine.setLayoutData(new GridData(SWT.FILL, SWT.CENTER, false, false, 2, 1));
final Label lblVersion = new Label(outerContainer, SWT.WRAP);
lblVersion.setLayoutData(new GridData(SWT.FILL, SWT.CENTER, false, false, 2, 1));
lblVersion.setText("Version 1.5.2 of 21 December 2015");
lblVersion.setBackground(backgroundColor);
}
public void standbyStateChanged(boolean standby) {
// do nothing for now (don't expect users to
// send welcome to standy)
}
public void setFocus() {
container.setFocus();
}
}
...@@ -11,7 +11,8 @@ Require-Bundle: org.eclipse.ui, ...@@ -11,7 +11,8 @@ Require-Bundle: org.eclipse.ui,
org.eclipse.debug.core;bundle-version="3.5.0", org.eclipse.debug.core;bundle-version="3.5.0",
org.eclipse.ui.editors;bundle-version="3.5.0", org.eclipse.ui.editors;bundle-version="3.5.0",
org.eclipse.jface.text;bundle-version="3.5.0", org.eclipse.jface.text;bundle-version="3.5.0",
org.eclipse.ui.console org.eclipse.ui.console,
org.lamport.tla.toolbox.product.standalone
Bundle-RequiredExecutionEnvironment: J2SE-1.5 Bundle-RequiredExecutionEnvironment: J2SE-1.5
Bundle-ActivationPolicy: lazy Bundle-ActivationPolicy: lazy
Import-Package: org.eclipse.ui.forms, Import-Package: org.eclipse.ui.forms,
......
package org.lamport.tla.toolbox.tool.prover; package org.lamport.tla.toolbox.tool.prover;
import org.lamport.tla.toolbox.tool.ToolboxLifecycleException; import org.lamport.tla.toolbox.lifecycle.ToolboxLifecycleParticipant;
import org.lamport.tla.toolbox.tool.ToolboxLifecycleParticipant;
import org.lamport.tla.toolbox.tool.prover.ui.util.ProverHelper; import org.lamport.tla.toolbox.tool.prover.ui.util.ProverHelper;
/** /**
...@@ -22,10 +21,8 @@ public class ProverToolboxLifecycleParticipant extends ToolboxLifecycleParticipa ...@@ -22,10 +21,8 @@ public class ProverToolboxLifecycleParticipant extends ToolboxLifecycleParticipa
/** /**
* Is called during termination of the toolbox. * Is called during termination of the toolbox.
* This implementation cancels all running prover jobs. * This implementation cancels all running prover jobs.
*
* @throws ToolboxLifecycleException
*/ */
public void terminate() throws ToolboxLifecycleException public void terminate()
{ {
ProverHelper.cancelProverJobs(true); ProverHelper.cancelProverJobs(true);
......
...@@ -12,7 +12,8 @@ Require-Bundle: org.eclipse.ui, ...@@ -12,7 +12,8 @@ Require-Bundle: org.eclipse.ui,
org.eclipse.jdt.launching;bundle-version="3.4.1", org.eclipse.jdt.launching;bundle-version="3.4.1",
org.eclipse.core.expressions;bundle-version="3.4.100", org.eclipse.core.expressions;bundle-version="3.4.100",
org.eclipse.ui.editors;bundle-version="3.5.0", org.eclipse.ui.editors;bundle-version="3.5.0",
org.eclipse.jface.text;bundle-version="3.5.0" org.eclipse.jface.text;bundle-version="3.5.0",
org.lamport.tla.toolbox.product.standalone
Bundle-RequiredExecutionEnvironment: J2SE-1.5 Bundle-RequiredExecutionEnvironment: J2SE-1.5
Bundle-ActivationPolicy: lazy Bundle-ActivationPolicy: lazy
Export-Package: org.lamport.tla.toolbox.tool.tlc.job, Export-Package: org.lamport.tla.toolbox.tool.tlc.job,
......
package org.lamport.tla.toolbox.tool.tlc; package org.lamport.tla.toolbox.tool.tlc;
import org.eclipse.core.runtime.jobs.Job; import org.eclipse.core.runtime.jobs.Job;
import org.lamport.tla.toolbox.tool.ToolboxLifecycleException; import org.lamport.tla.toolbox.lifecycle.ToolboxLifecycleParticipant;
import org.lamport.tla.toolbox.tool.ToolboxLifecycleParticipant;
import org.lamport.tla.toolbox.tool.tlc.job.TLCJob; import org.lamport.tla.toolbox.tool.tlc.job.TLCJob;
/** /**
...@@ -15,7 +14,7 @@ public class TLCLifecycleParticipant extends ToolboxLifecycleParticipant { ...@@ -15,7 +14,7 @@ public class TLCLifecycleParticipant extends ToolboxLifecycleParticipant {
/* (non-Javadoc) /* (non-Javadoc)
* @see org.lamport.tla.toolbox.tool.ToolboxLifecycleParticipant#terminate() * @see org.lamport.tla.toolbox.tool.ToolboxLifecycleParticipant#terminate()
*/ */
public void terminate() throws ToolboxLifecycleException { public void terminate() {
Job.getJobManager().cancel(TLCJob.AllJobsMatcher); Job.getJobManager().cancel(TLCJob.AllJobsMatcher);
} }
} }
...@@ -17,7 +17,8 @@ Require-Bundle: org.eclipse.ui, ...@@ -17,7 +17,8 @@ Require-Bundle: org.eclipse.ui,
org.eclipse.core.expressions;bundle-version="3.4.100", org.eclipse.core.expressions;bundle-version="3.4.100",
org.lamport.tlatools;bundle-version="1.0.0";visibility:=reexport, org.lamport.tlatools;bundle-version="1.0.0";visibility:=reexport,
org.eclipse.team.ui, org.eclipse.team.ui,
org.eclipse.core.filesystem;bundle-version="1.5.0" org.eclipse.core.filesystem;bundle-version="1.5.0",
org.lamport.tla.toolbox.product.standalone
Bundle-RequiredExecutionEnvironment: J2SE-1.5 Bundle-RequiredExecutionEnvironment: J2SE-1.5
Bundle-ActivationPolicy: lazy Bundle-ActivationPolicy: lazy
Bundle-ClassPath: ., Bundle-ClassPath: .,
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<?eclipse version="3.2"?> <?eclipse version="3.2"?>
<plugin> <plugin>
<extension-point id="org.lamport.tla.toolbox.tool" name="Toolbox Life Cycle Participant" schema="schema/org.lamport.tla.toolbox.tool.exsd"/>
<extension-point id="org.lamport.tla.toolbox.spec" name="Specification Life Cycle Participant" schema="schema/org.lamport.tla.toolbox.spec.exsd"/> <extension-point id="org.lamport.tla.toolbox.spec" name="Specification Life Cycle Participant" schema="schema/org.lamport.tla.toolbox.spec.exsd"/>
<!-- --> <!-- -->
<!-- Perspectives --> <!-- Perspectives -->
...@@ -1349,6 +1348,18 @@ ...@@ -1349,6 +1348,18 @@
class="org.lamport.tla.toolbox.util.pref.UnwantedPreferenceManager"> class="org.lamport.tla.toolbox.util.pref.UnwantedPreferenceManager">
</participant> </participant>
</extension> </extension>
<extension
point="org.lamport.tla.toolbox.tool">
<participant
class="org.lamport.tla.toolbox.ui.navigator.ToolboxExplorerResourceListener">
</participant>
</extension>
<extension
point="org.lamport.tla.toolbox.tool">
<participant
class="org.lamport.tla.toolbox.ui.view.ProblemViewResourceListener">
</participant>
</extension>
<!-- --> <!-- -->
<!-- Specification content --> <!-- Specification content -->
......
package org.lamport.tla.toolbox; package org.lamport.tla.toolbox;
import java.io.File;
import java.util.concurrent.CountDownLatch; import java.util.concurrent.CountDownLatch;
import org.eclipse.core.resources.IResourceChangeEvent; import org.eclipse.core.resources.IResourceChangeEvent;
...@@ -12,12 +11,8 @@ import org.eclipse.core.resources.WorkspaceJob; ...@@ -12,12 +11,8 @@ import org.eclipse.core.resources.WorkspaceJob;
import org.eclipse.core.runtime.CoreException; import org.eclipse.core.runtime.CoreException;
import org.eclipse.core.runtime.IProgressMonitor; import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.core.runtime.IStatus; import org.eclipse.core.runtime.IStatus;
import org.eclipse.core.runtime.Platform;
import org.eclipse.core.runtime.Status; import org.eclipse.core.runtime.Status;
import org.eclipse.core.runtime.jobs.Job; import org.eclipse.core.runtime.jobs.Job;
import org.eclipse.jface.dialogs.MessageDialog;
import org.eclipse.osgi.util.NLS;
import org.eclipse.ui.PlatformUI;
import org.lamport.tla.toolbox.spec.Spec; import org.lamport.tla.toolbox.spec.Spec;
import org.lamport.tla.toolbox.spec.manager.WorkspaceSpecManager; import org.lamport.tla.toolbox.spec.manager.WorkspaceSpecManager;
import org.lamport.tla.toolbox.spec.nature.TLAParsingBuilder.OutOfBuildSpecModulesGatheringDeltaVisitor; import org.lamport.tla.toolbox.spec.nature.TLAParsingBuilder.OutOfBuildSpecModulesGatheringDeltaVisitor;
...@@ -54,21 +49,6 @@ public class Activator extends AbstractTLCActivator ...@@ -54,21 +49,6 @@ public class Activator extends AbstractTLCActivator
super.start(context); super.start(context);
plugin = this; plugin = this;
// Only allow a single Toolbox instance per workspace to prevent data
// corruption in the workspace files.
if (!Platform.getInstanceLocation().lock()) {
final File workspaceDirectory = new File(Platform.getInstanceLocation().getURL().getFile());
if (workspaceDirectory.exists()) {
MessageDialog.openError(PlatformUI.createDisplay().getActiveShell(), "Toolbox files cannot be locked",
NLS.bind(
"Could not launch the Toolbox because the associated workspace is currently in use by another Toolbox. Opening two instances on the same workspace leads to data corruption.\n\n"
+ "If this is incorrect and there is no other Toolbox running, an earlier Toolbox terminated without releasing the lock. Please manually delete the lock file ''{0}'' and try restarting the Toolbox.",
workspaceDirectory.getAbsolutePath()
.concat(File.separator + ".metadata" + File.separator + ".lock")));
}
System.exit(1);
}
// register the listeners // register the listeners
IWorkspace workspace = ResourcesPlugin.getWorkspace(); IWorkspace workspace = ResourcesPlugin.getWorkspace();
...@@ -108,7 +88,7 @@ public class Activator extends AbstractTLCActivator ...@@ -108,7 +88,7 @@ public class Activator extends AbstractTLCActivator
getThread().wait(100); getThread().wait(100);
} }
} catch (InterruptedException e) { } catch (InterruptedException e) {
e.printStackTrace(); logError(e.getMessage(), e);
} }
state = context.getBundle().getState(); state = context.getBundle().getState();
} }
......
package org.lamport.tla.toolbox.tool;
/**
* Exception thrown during toolbox initialization or termination
* @author Simon Zambrovski
* @version $Id$
*/
public class ToolboxLifecycleException extends Exception
{
private static final long serialVersionUID = 6237014663324928734L;
public ToolboxLifecycleException(String message)
{
super(message);
}
public ToolboxLifecycleException(String message, Throwable cause)
{
super(message, cause);
}
}
...@@ -28,10 +28,6 @@ package org.lamport.tla.toolbox.ui.navigator; ...@@ -28,10 +28,6 @@ package org.lamport.tla.toolbox.ui.navigator;
import java.util.HashMap; import java.util.HashMap;
import java.util.Map; import java.util.Map;
import org.eclipse.core.resources.IResourceChangeEvent;
import org.eclipse.core.resources.IResourceChangeListener;
import org.eclipse.core.resources.IWorkspace;
import org.eclipse.core.resources.ResourcesPlugin;
import org.eclipse.jface.viewers.AbstractTreeViewer; import org.eclipse.jface.viewers.AbstractTreeViewer;
import org.eclipse.jface.viewers.DoubleClickEvent; import org.eclipse.jface.viewers.DoubleClickEvent;
import org.eclipse.jface.viewers.IStructuredSelection; import org.eclipse.jface.viewers.IStructuredSelection;
...@@ -125,7 +121,7 @@ public class ToolboxExplorer extends CommonNavigator ...@@ -125,7 +121,7 @@ public class ToolboxExplorer extends CommonNavigator
/** /**
* Refreshes the instance of the viewer if any * Refreshes the instance of the viewer if any
*/ */
private static void refresh() static void refresh()
{ {
CommonViewer instance = getViewer(); CommonViewer instance = getViewer();
if (instance != null) if (instance != null)
...@@ -159,47 +155,4 @@ public class ToolboxExplorer extends CommonNavigator ...@@ -159,47 +155,4 @@ public class ToolboxExplorer extends CommonNavigator
// contentService.update(); // contentService.update();
// } // }
// } // }
/*
* Use an inner class because instantiation of ProblemView itself should be
* left to the Eclipse foundation and not be triggered directly via new.
*/
public static class ResourceListener implements IResourceChangeListener {
private static ResourceListener INSTANCE;
public synchronized static void init() {
if (INSTANCE == null) {
INSTANCE = new ResourceListener();
}
}
private ResourceListener() {
// We might have missed events during Toolbox startup when there was
// a workspace but no UI yet.
resourceChanged(null);
// update CNF viewers
final IWorkspace workspace = ResourcesPlugin.getWorkspace();
workspace.addResourceChangeListener(this);
}
public void resourceChanged(final IResourceChangeEvent event) {
UIHelper.runUIAsync(new Runnable() {
public void run() {
ToolboxExplorer.refresh();
// Expand the current spec and all its children
final CommonViewer viewer = getViewer();
// Event is only null when this Ctor calls us causing the
// initial expanded state of a spec to be fully expanded.
// Afterwards, the users expanded states is preserved.
if (event == null && viewer != null) { // viewer might already be disposed which happens when the Toolbox shuts down.
final Spec specLoaded = Activator.getSpecManager().getSpecLoaded();
viewer.expandToLevel(specLoaded,
AbstractTreeViewer.ALL_LEVELS);
}
}
});
}
}
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment