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

Goto declaration can now also go to declarations in TLA+ standard 

modules.

Ctrl + Left Mouse on an operator - defined in a TLA+ standard module -
opens a read-only editor showing the corresponding standard module
and selects/reveals the actually definition of the operator.

[Feature][Toolbox][Changelog]
parent 667b2384
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
org.lamport.tla.toolbox.editor.basic/META-INF/MANIFEST.MF
+ 2
− 1
View file @ 103204a6
......@@ -14,7 +14,8 @@ Require-Bundle: org.eclipse.ui,
org.eclipse.core.resources,
org.eclipse.ui.workbench.texteditor,
org.eclipse.ui.views,
org.eclipse.ui.forms
org.eclipse.ui.forms,
org.eclipse.core.filesystem
Bundle-RequiredExecutionEnvironment: J2SE-1.5
Bundle-ActivationPolicy: lazy
Import-Package: org.eclipse.e4.core.services.events,
......
org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/actions/OpenDeclarationAction.java
+ 17
− 46
View file @ 103204a6
package org.lamport.tla.toolbox.editor.basic.actions;
import org.eclipse.core.resources.IFile;
import org.eclipse.core.resources.IResource;
import org.eclipse.core.runtime.IStatus;
import org.eclipse.core.runtime.Status;
import org.eclipse.jface.action.Action;
import org.eclipse.jface.text.IRegion;
import org.eclipse.jface.text.ITextSelection;
import org.eclipse.jface.text.hyperlink.IHyperlink;
import org.eclipse.jface.viewers.ISelection;
import org.eclipse.ui.part.FileEditorInput;
import org.eclipse.ui.IEditorInput;
import org.eclipse.ui.IEditorPart;
import org.lamport.tla.toolbox.editor.basic.TLAEditor;
import org.lamport.tla.toolbox.editor.basic.TLAEditorActivator;
import org.lamport.tla.toolbox.editor.basic.TLAEditorAndPDFViewer;
import org.lamport.tla.toolbox.editor.basic.util.EditorUtil;
import org.lamport.tla.toolbox.spec.Spec;
import org.lamport.tla.toolbox.tool.ToolboxHandle;
import org.lamport.tla.toolbox.util.UIHelper;
/**
......@@ -29,58 +21,38 @@ import org.lamport.tla.toolbox.util.UIHelper;
* nested class.
*
* @author Simon Zambrovski
* @version $Id$
*/
public class OpenDeclarationAction extends Action implements IHyperlink
{
private IResource resource;
private IRegion location;
private String label;
private final IEditorInput editorInput;
private final IRegion location;
private final String label;
private final IRegion hyperlinkLocation;
private final String editorId;
/**
* Constructs the action
* @param targetResource resource to link
* @param targetLocation location in the resource
* @param hyperlinkLabel label of the hyperlink
* @param hyperlinkLocation location of the hyperlink
*/
public OpenDeclarationAction(IResource targetResource, IRegion targetLocation, String hyperlinkLabel,
public OpenDeclarationAction(String editorId, IEditorInput editorInput, IRegion targetLocation, String hyperlinkLabel,
IRegion hyperlinkLocation)
{
super();
this.resource = targetResource;
this.editorId = editorId;
this.editorInput = editorInput;
this.location = targetLocation;
this.label = hyperlinkLabel;
this.hyperlinkLocation = hyperlinkLocation;
}
/**
* Action method
/* (non-Javadoc)
* @see org.eclipse.jface.action.Action#run()
*/
public void run()
{
TLAEditorActivator
.getDefault()
.getLog()
.log(new Status(IStatus.INFO, TLAEditorActivator.PLUGIN_ID,
"Opening " + label + "(" + resource.getName() + " at "
+ location + ")"));
EditorUtil.setReturnFromOpenDecl();
// // Find current location and store as a property of the spec for the
// // Return from Goto Declaration command.
// TLAEditor srcEditor = EditorUtil.getTLAEditorWithFocus();
// if (srcEditor != null)
// {
// Spec spec = ToolboxHandle.getCurrentSpec();
// spec.setOpenDeclModuleName(srcEditor.getEditorInput().getName());
// spec.setOpenDeclSelection((ITextSelection) srcEditor.getSelectionProvider().getSelection());
// }
TLAEditorAndPDFViewer editor = (TLAEditorAndPDFViewer) UIHelper.openEditor(TLAEditorAndPDFViewer.ID,
new FileEditorInput((IFile) resource));
editor.getTLAEditor().selectAndReveal(location.getOffset(), location.getLength());
final IEditorPart editor = UIHelper.openEditor(editorId, editorInput);
if (editor instanceof TLAEditorAndPDFViewer) {
((TLAEditorAndPDFViewer) editor).getTLAEditor().selectAndReveal(location.getOffset(), location.getLength());
} else if (editor instanceof TLAEditor) {
((TLAEditor) editor).selectAndReveal(location.getOffset(), location.getLength());
}
}
/* (non-Javadoc)
......@@ -114,5 +86,4 @@ public class OpenDeclarationAction extends Action implements IHyperlink
{
run();
}
}
org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/tla/TLAHyperlinkDetector.java
+ 47
− 20
View file @ 103204a6
package org.lamport.tla.toolbox.editor.basic.tla;
import java.io.File;
import org.eclipse.core.filesystem.EFS;
import org.eclipse.core.filesystem.IFileStore;
import org.eclipse.core.resources.IFile;
import org.eclipse.core.resources.IResource;
import org.eclipse.core.runtime.CoreException;
import org.eclipse.core.runtime.Path;
import org.eclipse.jface.text.BadLocationException;
import org.eclipse.jface.text.IDocument;
import org.eclipse.jface.text.IRegion;
......@@ -10,9 +14,15 @@ import org.eclipse.jface.text.ITextViewer;
import org.eclipse.jface.text.Region;
import org.eclipse.jface.text.hyperlink.AbstractHyperlinkDetector;
import org.eclipse.jface.text.hyperlink.IHyperlink;
import org.eclipse.ui.IEditorInput;
import org.eclipse.ui.editors.text.FileDocumentProvider;
import org.eclipse.ui.editors.text.TextFileDocumentProvider;
import org.eclipse.ui.ide.FileStoreEditorInput;
import org.eclipse.ui.part.FileEditorInput;
import org.eclipse.ui.texteditor.IDocumentProvider;
import org.lamport.tla.toolbox.editor.basic.TLAEditorActivator;
import org.lamport.tla.toolbox.editor.basic.TLAEditorAndPDFViewer;
import org.lamport.tla.toolbox.editor.basic.TLAEditorReadOnly;
import org.lamport.tla.toolbox.editor.basic.actions.OpenDeclarationAction;
import org.lamport.tla.toolbox.tool.ToolboxHandle;
import org.lamport.tla.toolbox.util.ResourceHelper;
......@@ -23,6 +33,7 @@ import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.SymbolNode;
import tla2sany.semantic.ThmOrAssumpDefNode;
import tla2sany.st.SyntaxTreeConstants;
import util.FilenameToStream;
/**
* Detects hyperlinks in TLA+ code
......@@ -87,6 +98,7 @@ public class TLAHyperlinkDetector extends AbstractHyperlinkDetector
return null;
}
// Set region to the Region of the document described by currentTokenSpec
// (this ugly re-use of a parameter name is kept from Simon's original
// code), set label to the found symbol name, and set resolvedSymbol to
......@@ -127,25 +139,40 @@ public class TLAHyperlinkDetector extends AbstractHyperlinkDetector
TLAEditorActivator.getDefault().logDebug(csNode.getAttachedComments()[i]);
}
IResource resource = null;
IDocumentProvider documentProvider = null;
IEditorInput editorInput = null;
String editorId = "";
//
if (ToolboxHandle.isUserModule(ResourceHelper.getModuleFileName(csNode.getFilename())))
{
// resource
resource = ResourceHelper.getResourceByModuleName(csNode.getFilename());
} else
{
// TLAEditorActivator.getDefault().logDebug("A StandardModule '" + csNode.getFilename() + "' is requested...");
final FilenameToStream resolver = ToolboxHandle.getSpecObj().getResolver();
if (ToolboxHandle.isUserModule(ResourceHelper.getModuleFileName(csNode.getFilename()))) {
editorId = TLAEditorAndPDFViewer.ID;
editorInput = new FileEditorInput(
(IFile) ResourceHelper.getResourceByModuleName(csNode.getFilename()));
documentProvider = new FileDocumentProvider();
} else if (resolver.isStandardModule(csNode.getFilename())) {
// No point editing standard modules.
editorId = TLAEditorReadOnly.ID;
// Resolve the file via the FilenameToStream resolver in case a user has
// provided its own standard module definition.
final File resolved = resolver.resolve(csNode.getFilename(), true);
// Standard modules live outside the workspace which is why they have to be
// opened with EFS and read with a TextFileDocumentProvider.
final IFileStore fileStore = EFS.getLocalFileSystem()
.getStore(new Path(resolved.getAbsolutePath()));
editorInput = new FileStoreEditorInput(fileStore);
documentProvider = new TextFileDocumentProvider();
} else {
// A TLA+ built-in module.
return null;
}
// connect to the resource
FileEditorInput fileEditorInput = new FileEditorInput((IFile) resource);
FileDocumentProvider fileDocumentProvider = new FileDocumentProvider();
try
{
fileDocumentProvider.connect(fileEditorInput);
document = fileDocumentProvider.getDocument(fileEditorInput);
documentProvider.connect(editorInput);
document = documentProvider.getDocument(editorInput);
} finally
{
/*
......@@ -155,7 +182,7 @@ public class TLAHyperlinkDetector extends AbstractHyperlinkDetector
* Keeping it connected only seems to provide synchronization of
* the document with file changes. That is not necessary in this context.
*/
fileDocumentProvider.disconnect(fileEditorInput);
documentProvider.disconnect(editorInput);
}
try
......@@ -164,7 +191,7 @@ public class TLAHyperlinkDetector extends AbstractHyperlinkDetector
// to get just the symbol from the left-hand side. (Otherwise,
// the user can't execute Goto Declaration immediately followed
// by Show Uses.)
if (resolvedSymbol instanceof OpDefNode)
if (resolvedSymbol instanceof OpDefNode && csNode.getHeirs().length >= 1)
{
// Need to pick out the symbol from the left-hand side of
// the definition.
......@@ -180,7 +207,7 @@ public class TLAHyperlinkDetector extends AbstractHyperlinkDetector
csNode = csNode.getHeirs()[1];
}
}
} else if ((resolvedSymbol instanceof ThmOrAssumpDefNode)
} else if ((resolvedSymbol instanceof ThmOrAssumpDefNode && csNode.getHeirs().length >= 2)
&& ((csNode.getKind() == SyntaxTreeConstants.N_Theorem) || (csNode.getKind() == SyntaxTreeConstants.N_Assumption)))
{
csNode = csNode.getHeirs()[1];
......@@ -192,7 +219,7 @@ public class TLAHyperlinkDetector extends AbstractHyperlinkDetector
int startOffset = startLineRegion.getOffset() + csNode.getLocation().beginColumn() - 1;
int endOffset = endLineRegion.getOffset() + csNode.getLocation().endColumn();
return new IHyperlink[] { new OpenDeclarationAction(resource, new Region(startOffset, endOffset
return new IHyperlink[] { new OpenDeclarationAction(editorId, editorInput, new Region(startOffset, endOffset
- startOffset), label, region) };
} catch (BadLocationException e)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment