F3 shortcut does not work for identifiers in subscripts.

Fixes Github issue #106
https://github.com/tlaplus/tlaplus/issues/106

[Bug][Toolbox]

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

@@ -20,4 +20,5 @@ Bundle-ActivationPolicy: lazy
 Import-Package: org.eclipse.e4.core.services.events,
  org.eclipse.ui.forms
 Export-Package: org.lamport.tla.toolbox.editor.basic,
+ org.lamport.tla.toolbox.editor.basic.tla,
  org.lamport.tla.toolbox.editor.basic.util

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/tla/TLAHyperlinkDetector.java

@@ -12,27 +12,17 @@ import org.eclipse.jface.text.hyperlink.AbstractHyperlinkDetector;
 import org.eclipse.jface.text.hyperlink.IHyperlink;
 import org.eclipse.ui.editors.text.FileDocumentProvider;
 import org.eclipse.ui.part.FileEditorInput;
-import org.lamport.tla.toolbox.editor.basic.TLAEditor;
 import org.lamport.tla.toolbox.editor.basic.TLAEditorActivator;
 import org.lamport.tla.toolbox.editor.basic.actions.OpenDeclarationAction;
-import org.lamport.tla.toolbox.editor.basic.util.DocumentHelper;
-import org.lamport.tla.toolbox.editor.basic.util.EditorUtil;
-import org.lamport.tla.toolbox.editor.basic.util.EditorUtil.StringAndLocation;
 import org.lamport.tla.toolbox.tool.ToolboxHandle;
-import org.lamport.tla.toolbox.ui.handler.OpenModuleHandler;
 import org.lamport.tla.toolbox.util.ResourceHelper;
 
-import tla2sany.modanalyzer.SpecObj;
 import tla2sany.parser.SyntaxTreeNode;
-import tla2sany.parser.TLAplusParserConstants;
-import tla2sany.semantic.Context;
 import tla2sany.semantic.ModuleNode;
 import tla2sany.semantic.OpDefNode;
 import tla2sany.semantic.SymbolNode;
 import tla2sany.semantic.ThmOrAssumpDefNode;
-import tla2sany.st.Location;
 import tla2sany.st.SyntaxTreeConstants;
-import util.UniqueString;
 
 /**
  * Detects hyperlinks in TLA+ code
@@ -50,10 +40,6 @@ import util.UniqueString;
 public class TLAHyperlinkDetector extends AbstractHyperlinkDetector
 {
 
-    public TLAHyperlinkDetector()
-    {
-    }
-
     /**
      * This method first sets label to the token at the position indicated by the
      * region.  If the module is parsed and unmodified, it uses EditorUtil.getTokenAt

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/tla/TokenSpec.java

@@ -148,9 +148,15 @@ public class TokenSpec
             int rightPos = tokenSpecs[i].rightPos;
             tokenSpecs[i].leftPos = leftPos + offsetOfLine;
             tokenSpecs[i].rightPos = rightPos + offsetOfLine;
+
+            String indiceAdjustedToken = tokenSpecs[i].token;
             Location location = EditorUtil.getLocationAt(document, tokenSpecs[i].leftPos, rightPos - leftPos);
-            symbol = EditorUtil.lookupOriginalSymbol(UniqueString.uniqueStringOf(tokenSpecs[i].token), moduleNode,
-                    location, null);
+            
+            if ((indiceAdjustedToken != null) && (indiceAdjustedToken.length() > 1) && (indiceAdjustedToken.charAt(0) == '_')) {
+                indiceAdjustedToken = indiceAdjustedToken.substring(1);
+            }
+            
+            symbol = EditorUtil.lookupOriginalSymbol(UniqueString.uniqueStringOf(indiceAdjustedToken), moduleNode, location, null);
             if (symbol != null)
             {
                 goodIndex = i;

org.lamport.tla.toolbox.tool.tlc.ui.uitest/META-INF/MANIFEST.MF

@@ -12,7 +12,9 @@ Require-Bundle: org.lamport.tla.toolbox;bundle-version="1.0.0",
  org.eclipse.core.resources;bundle-version="3.5.0",
  org.eclipse.debug.core;bundle-version="3.5.0",
  org.eclipse.ui.editors;bundle-version="3.6.0",
- org.eclipse.ui.workbench
+ org.eclipse.ui.workbench,
+ org.eclipse.jface.text;bundle-version="3.12.0",
+ org.apache.commons.io;bundle-version="2.0.1"
 Import-Package: org.osgi.framework;version="1.3.0"
 Bundle-RequiredExecutionEnvironment: J2SE-1.5
 Bundle-Vendor: Leslie Lamport, Markus Alexander Kuppe

org.lamport.tla.toolbox.tool.tlc.ui.uitest/pom.xml

@@ -54,6 +54,7 @@
 
 					<systemProperties combine.children="append">
 						<!-- References used by tests to access spec files -->
+						<org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecC>${project.build.directory}/../../org.lamport.tla.toolbox.uitest/farsite/GotoDefinition.tla</org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecC>
 						<org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecB>${project.build.directory}/../../org.lamport.tla.toolbox.uitest/farsite/DistributedSystemModule.tla</org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecB>
 						<org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecA>${project.build.directory}/../../org.lamport.tla.toolbox.uitest/DieHard/DieHard.tla</org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecA>
 						<!-- JDT weaving debug output -->

org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/tool/tlc/ui/test/AbstractTest.java

@@ -17,7 +17,11 @@ import org.eclipse.ui.PlatformUI;
 import org.hamcrest.Matcher;
 import org.junit.Assert;
 import org.junit.Before;
+import org.lamport.tla.toolbox.Activator;
+import org.lamport.tla.toolbox.spec.Spec;
 import org.lamport.tla.toolbox.test.RCPTestSetupHelper;
+import org.lamport.tla.toolbox.tool.tlc.model.Model;
+import org.lamport.tla.toolbox.tool.tlc.model.TLCSpec;
 
 public abstract class AbstractTest {
 
@@ -51,6 +55,7 @@ public abstract class AbstractTest {
 	/**
 	 * Pre flight initialization (run once for each test _case_)
 	 */
+	@SuppressWarnings("unchecked") // Generics in WidgetMatcherFactory.allOf invocation
 	@Before
 	public void setUp() throws Exception {
 		// Force shell activation to counter, no active Shell when running SWTBot tests in Xvfb/Xvnc
@@ -92,4 +97,20 @@ public abstract class AbstractTest {
 		bot.waitUntil(waitForShell);
 		return new SWTBotShell(waitForShell.get(0));
 	}
+
+    /**
+     * Verifies that the spec and model show expected state (via API!!!)
+     * 
+     * @param modelName if null, the model's existence will not be checked
+     */
+    protected void checkSpecAndModelExistenceAPI(final String expectedSpecName, final String modelName) {
+        final Spec spec = Activator.getSpecManager().getSpecLoaded();
+        Assert.assertEquals(expectedSpecName, spec.getName());
+        
+        if (modelName != null) {
+            final Model model = spec.getAdapter(TLCSpec.class).getModel(modelName);
+            Assert.assertNotNull("Model could not be found", model);
+        }
+    }
+
 }

org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/ui/handler/CloneModelTest.java

@@ -8,15 +8,11 @@ import org.eclipse.swtbot.swt.finder.junit.SWTBotJunit4ClassRunner;
 import org.eclipse.swtbot.swt.finder.matchers.WithText;
 import org.eclipse.swtbot.swt.finder.waits.Conditions;
 import org.eclipse.swtbot.swt.finder.widgets.SWTBotMenu;
-import org.junit.Assert;
+
 import org.junit.Before;
 import org.junit.BeforeClass;
 import org.junit.Test;
 import org.junit.runner.RunWith;
-import org.lamport.tla.toolbox.Activator;
-import org.lamport.tla.toolbox.spec.Spec;
-import org.lamport.tla.toolbox.tool.tlc.model.Model;
-import org.lamport.tla.toolbox.tool.tlc.model.TLCSpec;
 import org.lamport.tla.toolbox.tool.tlc.ui.test.AbstractTest;
 import org.lamport.tla.toolbox.tool.tlc.ui.test.ModelEditorOpenCondition;
 
@@ -65,7 +61,7 @@ public class CloneModelTest extends AbstractTest {
 		SWTBotEditor activeEditor = bot.activeEditor();
 		activeEditor.saveAndClose();
 		
-		checkSpecAndModelExistenceAPI(TEST_SPEC);
+		checkSpecAndModelExistenceAPI(TEST_SPEC, TEST_MODEL);
 	}
 
 	@Test
@@ -79,12 +75,4 @@ public class CloneModelTest extends AbstractTest {
 		bot.waitUntil(new ModelEditorOpenCondition(TEST_MODEL_RENAME));
 	}
 
-	// Verify spec and model show expected state (via API!!!)
-	private void checkSpecAndModelExistenceAPI(final String specExpected) {
-		final Spec spec = Activator.getSpecManager().getSpecLoaded();
-		Assert.assertEquals(specExpected, spec.getName());
-		
-		final Model model = spec.getAdapter(TLCSpec.class).getModel(TEST_MODEL);
-		Assert.assertNotNull("Model could not be found", model);
-	}
 }

org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/ui/handler/GotoDefinitionTest.java

+package org.lamport.tla.toolbox.ui.handler;
+
+import java.io.File;
+import java.io.FileInputStream;
+import java.io.FileOutputStream;
+import java.util.ArrayList;
+
+import org.apache.commons.io.IOUtils;
+
+import org.eclipse.jface.text.Region;
+import org.eclipse.swt.widgets.MenuItem;
+import org.eclipse.swtbot.eclipse.finder.widgets.SWTBotEditor;
+import org.eclipse.swtbot.swt.finder.junit.SWTBotJunit4ClassRunner;
+import org.eclipse.swtbot.swt.finder.matchers.WithText;
+import org.eclipse.swtbot.swt.finder.utils.FileUtils;
+import org.eclipse.swtbot.swt.finder.waits.Conditions;
+import org.eclipse.swtbot.swt.finder.widgets.SWTBotMenu;
+
+import org.junit.Assert;
+import org.junit.Before;
+import org.junit.BeforeClass;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.lamport.tla.toolbox.editor.basic.tla.TokenSpec;
+import org.lamport.tla.toolbox.test.RCPTestSetupHelper;
+import org.lamport.tla.toolbox.tool.tlc.ui.test.AbstractTest;
+import org.lamport.tla.toolbox.util.UIHelper;
+
+
+/**
+ * This test started life to provide test cases related to GitHub issue #106.
+ */
+@RunWith(SWTBotJunit4ClassRunner.class)
+public class GotoDefinitionTest extends AbstractTest {
+	
+	private static final String TEST_SPEC_NAME = "GotoDefinition";
+	private static final String REPOSITORY_SPEC_PATH = System.getProperty("org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpec",
+	                                                                      RCPTestSetupHelper.getAbsolutePath("org.lamport.tla.toolbox.uitest",
+	                                                                                                         "farsite/GotoDefinition.tla"));
+
+	@BeforeClass
+	public static void beforeClass () {
+		// mimic super
+		AbstractTest.beforeClass();
+	}
+
+	@Before
+	public void setUp () throws Exception {
+		super.setUp();
+
+		// load our known spec
+		SWTBotMenu fileMenu = bot.menu("File");
+		SWTBotMenu openSpecMenu = fileMenu.menu("Open Spec");
+		SWTBotMenu addNewSpecMenu = openSpecMenu.menu("Add New Spec...");
+		addNewSpecMenu.click();
+		
+		String path = System.getProperty("java.io.tmpdir") + File.separator + "GDTest" + System.currentTimeMillis();
+		FileUtils.mkdirs(path);
+		
+		// Put a copy of the spec into our temporary working directory
+		path += File.separator + TEST_SPEC_NAME + TLA_SUFFIX;
+		FileInputStream fis = null;
+		FileOutputStream fos = null;
+		try {
+		    fis = new FileInputStream(REPOSITORY_SPEC_PATH);
+		    fos = new FileOutputStream(path);
+		    
+		    IOUtils.copy(fis, fos);
+		}
+		finally {
+		    IOUtils.closeQuietly(fis);
+		    IOUtils.closeQuietly(fos);
+		}
+
+		bot.textWithLabel("Root-module file:").setText(path);
+		bot.button("Finish").click();
+
+		bot.waitUntil(Conditions.waitForMenu(bot.activeShell(), WithText.<MenuItem> withText(TEST_SPEC_NAME)));
+		
+		checkSpecAndModelExistenceAPI(TEST_SPEC_NAME, null);
+	}
+	
+	/**
+	 * See first issue mentioned in https://github.com/tlaplus/tlaplus/issues/106
+	 * 
+	 * We don't need to test the hyperlink jump, we only need to test that the TokenSpec instance returned by
+	 *     TokenSpec.findCurrentTokenSpec(IRegion) has a non-null resolvedSymbol attribute.
+	 */
+	@Test
+	public void verifyTokenSpecSymbolResolution () {
+	    // This region is expected to place the cursor just prior to the subscripted identifier, the 's' in "..._s" in:
+	    //             Spec == s = "" /\ [][Next(s)]_s
+	    final Region r = new Region(193, 0);
+	    final ArrayList<TokenSpec> crossThreadSmuggler = new ArrayList<>();
+	    final Runnable uiRunnable = new Runnable () {
+	        public void run () {
+	            TokenSpec ts = TokenSpec.findCurrentTokenSpec(r);
+	            
+	            synchronized (crossThreadSmuggler) {
+	                crossThreadSmuggler.add(ts);
+	            }
+	        }
+	    };
+	    final TokenSpec ts;
+	    int size = 0;
+	    int waitCycles = 0;
+
+	    UIHelper.runUIAsync(uiRunnable);
+	    while ((size == 0) && (waitCycles < 15)) {
+	        try {
+	            Thread.sleep(575);
+	        }
+	        catch (Exception e) { } // NOPMD
+	        
+	        waitCycles++;
+	        synchronized (crossThreadSmuggler) {
+	            size = crossThreadSmuggler.size();
+	        }
+	    }
+
+	    Assert.assertNotEquals("We timed out waiting for the TokenSpec find.", 0, size);
+	    
+	    ts = crossThreadSmuggler.get(0);
+	    
+	    Assert.assertNotNull("TokenSpec was unable to find any token at " + r.toString(), ts);
+	    
+	    Assert.assertEquals("TokenSpec was not for the expected token, perhaps someone has changed GotoDefinition.tla?", "_s",
+	                        ts.token);
+
+	    Assert.assertNotNull("TokenSpec was unable to resolve the symbol for the token [" + ts.token + "] at " + r.toString(),
+	                         ts.resolvedSymbol);
+	    
+	    // No real reason this need be done from a test functionality perspective
+        SWTBotEditor activeEditor = bot.activeEditor();
+        activeEditor.close();
+	}
+
+}

org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/ui/handler/RenameSpecHandlerTest.java

@@ -16,13 +16,12 @@ import org.eclipse.swtbot.swt.finder.waits.ICondition;
 import org.eclipse.swtbot.swt.finder.widgets.SWTBotMenu;
 import org.eclipse.swtbot.swt.finder.widgets.SWTBotTreeItem;
 import org.eclipse.ui.IEditorPart;
+
 import org.junit.Assert;
 import org.junit.Before;
 import org.junit.BeforeClass;
 import org.junit.Test;
 import org.junit.runner.RunWith;
-import org.lamport.tla.toolbox.Activator;
-import org.lamport.tla.toolbox.spec.Spec;
 import org.lamport.tla.toolbox.tool.ToolboxHandle;
 import org.lamport.tla.toolbox.tool.tlc.model.Model;
 import org.lamport.tla.toolbox.tool.tlc.model.TLCSpec;
@@ -80,7 +79,7 @@ public class RenameSpecHandlerTest extends AbstractTest {
 		SWTBotEditor activeEditor = bot.activeEditor();
 		activeEditor.saveAndClose();
 		
-		checkSpecAndModelExistenceAPI(TEST_SPEC);
+		checkSpecAndModelExistenceAPI(TEST_SPEC, TEST_MODEL);
 	}
 	
 	/**
@@ -103,7 +102,7 @@ public class RenameSpecHandlerTest extends AbstractTest {
 		bot.waitUntil(new SpecEditorOpenCondition(TEST_SPEC));
 
 		// verify (via API)
-		checkSpecAndModelExistenceAPI(TEST_SPEC + "_Copy");
+		checkSpecAndModelExistenceAPI((TEST_SPEC + "_Copy"), TEST_MODEL);
 		
 		// try to find the renamed file (via UI)
 		openSpecExplorer();
@@ -145,16 +144,6 @@ public class RenameSpecHandlerTest extends AbstractTest {
 		}
 	}
 	
-	// Verify spec and model show expected state (via API!!!)
-	private void checkSpecAndModelExistenceAPI(final String specExpected) {
-		final Spec spec = Activator.getSpecManager().getSpecLoaded();
-		Assert.assertEquals(specExpected, spec.getName());
-		
-		
-		final Model model = spec.getAdapter(TLCSpec.class).getModel(TEST_MODEL);
-		Assert.assertNotNull("Model could not be found", model);
-	}
-	
 	// check if the models have been renamed correctly too (via UI!!!)
 	private SWTBotTreeItem checkForModelExistenceUI(final SWTBotTreeItem treeItem) {
 		try {

org.lamport.tla.toolbox.uitest/farsite/GotoDefinition.tla

+--------------------------- MODULE GotoDefinition ---------------------------
+EXTENDS Integers
+VARIABLE s
+
+Next(var) == \E val \in 0..1: (var' = val /\ var' > 0)
+
+Spec == s = "" /\ [][Next(s)]_s
+
+=============================================================================