Prevent multiple Toolbox instances from running simultaneously.

Running multiple Toolbox instances can lead to data corruption and thus should be prevented.

The primary use case for having multiple instances open, is to study files of spec A while working on B. File > Open Module > Add TLA+ module has been extended to open files from spec A in read-only mode.

[Bug][Toolbox[Changelog]

org.lamport.tla.toolbox/META-INF/MANIFEST.MF

@@ -16,7 +16,8 @@ Require-Bundle: org.eclipse.ui,
  org.eclipse.ui.navigator;bundle-version="3.3.101";visibility:=reexport,
  org.eclipse.core.expressions;bundle-version="3.4.100",
  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"
 Bundle-RequiredExecutionEnvironment: J2SE-1.5
 Bundle-ActivationPolicy: lazy
 Bundle-ClassPath: .,

org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/Activator.java

 package org.lamport.tla.toolbox;
 
+import java.io.File;
 import java.util.concurrent.CountDownLatch;
 
 import org.eclipse.core.resources.IResourceChangeEvent;
@@ -11,8 +12,12 @@ import org.eclipse.core.resources.WorkspaceJob;
 import org.eclipse.core.runtime.CoreException;
 import org.eclipse.core.runtime.IProgressMonitor;
 import org.eclipse.core.runtime.IStatus;
+import org.eclipse.core.runtime.Platform;
 import org.eclipse.core.runtime.Status;
 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.manager.WorkspaceSpecManager;
 import org.lamport.tla.toolbox.spec.nature.TLAParsingBuilder.OutOfBuildSpecModulesGatheringDeltaVisitor;
@@ -49,6 +54,21 @@ public class Activator extends AbstractTLCActivator
         super.start(context);
         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
         IWorkspace workspace = ResourcesPlugin.getWorkspace();
         

org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/handler/AddModuleHandler.java

@@ -7,6 +7,8 @@ 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.filesystem.EFS;
+import org.eclipse.core.filesystem.IFileStore;
 import org.eclipse.core.resources.IFile;
 import org.eclipse.core.resources.ResourcesPlugin;
 import org.eclipse.core.runtime.CoreException;
@@ -16,6 +18,7 @@ import org.eclipse.jface.dialogs.MessageDialog;
 import org.eclipse.swt.widgets.FileDialog;
 import org.eclipse.ui.IWorkbenchWindow;
 import org.eclipse.ui.handlers.HandlerUtil;
+import org.eclipse.ui.ide.FileStoreEditorInput;
 import org.lamport.tla.toolbox.Activator;
 import org.lamport.tla.toolbox.spec.Spec;
 import org.lamport.tla.toolbox.util.ResourceHelper;
@@ -83,15 +86,28 @@ public class AddModuleHandler extends AbstractHandler implements IHandler
                     // check the folder we are in
                     if (!ResourceHelper.isProjectParent(modulePath.removeLastSegments(1), spec.getProject()))
                     {
-                        // the selected resource is not in the same directory as the root file
-                        MessageDialog
-                                .openInformation(
-                                        window.getShell(),
-                                        "Wrong TLA+ Module is part of the spec",
-                                        "The provided module "
-                                                + module.getName()
-                                                + " is not located in the same directory as the root file. \nPlease select the module in "
-                                                + spec.getRootFile().getFullPath().removeLastSegments(1).toOSString());
+						// the selected resource is not in the same directory as
+						// the root file
+						MessageDialog.openInformation(window.getShell(), "TLA+ Module is not part of the current spec.",
+								"The provided module " + module.getName()
+										+ " is not part of the spec which is currently open. It will therefore be opened in read-only mode.\n"
+										+ "If you want to make changes to this file, you will have to open the corresponding spec first.");
+
+						// Open TLA's read-only editor on a .tla file that does
+						// *not* belong to the current spec. It is opened
+						// read-only, because we want to allow any changes,
+						// because we couldn't parse the spec anyway. The reason
+						// why this functionality is offered, is to allow users
+						// to look at .tla files of closed spec.
+						// http://wiki.eclipse.org/FAQ_How_do_I_open_an_editor_on_a_file_outside_the_workspace%3F
+						final IFileStore fileStore = EFS.getLocalFileSystem().getStore(new Path(moduleFileName));
+						if (!fileStore.fetchInfo().isDirectory() && fileStore.fetchInfo().exists()) {
+							UIHelper.openEditor("org.lamport.tla.toolbox.editor.basic.TLAEditorReadOnly",
+									new FileStoreEditorInput(fileStore));
+						} else {
+							throw new ExecutionException(moduleFileName
+									+ " cannot be opened in read-only mode because its file content could not be obtained.");
+						}
                         return null;
                     }