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

Automatically translate PlusCal to TLA+. 

Toggle automatic translation via editor's right-click context menu.

[Feature][Toolbox][Changelog]
parent 9bd518ca
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 259 additions and 98 deletions
org.lamport.tla.toolbox.editor.basic/META-INF/MANIFEST.MF
+ 2
− 1
View file @ 642b540e
......@@ -19,7 +19,8 @@ Require-Bundle: org.eclipse.ui,
Bundle-RequiredExecutionEnvironment: JavaSE-1.8
Bundle-ActivationPolicy: lazy
Import-Package: org.eclipse.e4.core.services.events,
org.eclipse.ui.forms
org.eclipse.ui.forms,
org.osgi.service.event;version="1.3.1"
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/plugin.xml
+ 19
− 0
View file @ 642b540e
......@@ -307,6 +307,17 @@
id="org.lamport.tla.toolbox.editor.basic.DecomposeProof"
name="Decompose Proof">
</command>
<command
categoryId="org.eclipse.ui.category.textEditor"
defaultHandler="org.lamport.tla.toolbox.editor.basic.handlers.PCalTranslateAutomaticallyHandler"
description="Automatically translate PlusCal to TLA+ on TLA+ editor save."
id="toolbox.command.module.translate.automatially"
name="Translate PlusCal automatically">
<state
class="org.eclipse.ui.handlers.RegistryToggleState:false"
id="org.eclipse.ui.commands.toggleState">
</state>
</command>
<command
categoryId="toolbox.command.category.module"
defaultHandler="org.lamport.tla.toolbox.editor.basic.handlers.PCalTranslateModuleHandler"
......@@ -636,6 +647,14 @@
commandId="org.lamport.tla.toolbox.editor.basic.gotoMatchingParen"
style="push">
</command>
<separator
name="org.lamport.tla.toolbox.editor.basic.commentseparator"
visible="true">
</separator>
<command
commandId="toolbox.command.module.translate.automatially"
style="toggle">
</command>
</menuContribution>
</extension>
......
org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/TLAEditor.java
+ 7
− 0
View file @ 642b540e
......@@ -109,6 +109,11 @@ public class TLAEditor extends TextEditor
* saved.
*/
public static final String SAVE_EVENT = "TLAEditor/save";
/**
* The IEventBroker topic identifying the event sent out while the editor is
* being saved.
*/
public static final String PRE_SAVE_EVENT = "TLAEditor/presave";
public static final String ID = "org.lamport.tla.toolbox.editor.basic.TLAEditor";
private IContextService contextService = null;
......@@ -446,6 +451,8 @@ public class TLAEditor extends TextEditor
*/
public void doSave(IProgressMonitor progressMonitor)
{
service.send(PRE_SAVE_EVENT, this);
final IEditorInput editorInput = this.getEditorInput();
IDocument doc = this.getDocumentProvider().getDocument(editorInput);
String text = doc.get();
......
org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/handlers/PCalTranslateAutomaticallyHandler.java 0 → 100644
+ 97
− 0
View file @ 642b540e
/*******************************************************************************
* Copyright (c) 2018 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.editor.basic.handlers;
import java.lang.reflect.InvocationTargetException;
import org.eclipse.core.commands.Command;
import org.eclipse.core.commands.ExecutionEvent;
import org.eclipse.core.commands.ExecutionException;
import org.eclipse.core.commands.State;
import org.eclipse.e4.core.services.events.IEventBroker;
import org.eclipse.ui.PlatformUI;
import org.eclipse.ui.commands.ICommandService;
import org.eclipse.ui.handlers.HandlerUtil;
import org.eclipse.ui.handlers.RegistryToggleState;
import org.lamport.tla.toolbox.editor.basic.TLAEditor;
import org.lamport.tla.toolbox.editor.basic.pcal.PCalTranslator;
import org.osgi.service.event.Event;
import org.osgi.service.event.EventHandler;
public class PCalTranslateAutomaticallyHandler extends PCalTranslator implements EventHandler {
public PCalTranslateAutomaticallyHandler() {
// This IHander is stateful even across Toolbox restarts. In other words, if the
// user requests automatic PlusCal translation, it will enabled even after a
// Toolbox restart. This means we have to register this at the IEventBroker
// during Toolbox startup.
// It is vital that we use the Workbench's IEventBroker instance. If e.g. we
// would use an IEventBroker from higher up the IEclipseContext hierarchy, the
// broker would be disposed when a new spec gets opened but the IHandler's state
// remains enabled.
final IEventBroker service = PlatformUI.getWorkbench().getService(IEventBroker.class);
service.subscribe(TLAEditor.PRE_SAVE_EVENT, this);
}
/* (non-Javadoc)
* @see org.eclipse.core.commands.IHandler#execute(org.eclipse.core.commands.ExecutionEvent)
*/
public Object execute(final ExecutionEvent event) throws ExecutionException {
// Toggle the IHandler's state at the UI level (check mark on/off). The
// IEventBroker handler remains subscribed to the event bus but will simply
// ignore the events.
HandlerUtil.toggleCommandState(event.getCommand());
return null;
}
/* (non-Javadoc)
* @see org.osgi.service.event.EventHandler#handleEvent(org.osgi.service.event.Event)
*/
@Override
public void handleEvent(final Event event) {
if (!isAutomaticEnabled()) {
// If the UI state is false, the user doesn't want automatic PlusCal translation.
return;
}
try {
final TLAEditor editor = (TLAEditor) event.getProperty(IEventBroker.DATA);
translate(editor, editor.getSite().getShell(), false);
} catch (InvocationTargetException | InterruptedException e) {
throw new RuntimeException(e);
}
}
/*
* Check the UI state of the IHandler/Command which indicates if the user
* enabled automatic PlusCal conversion.
*/
private static boolean isAutomaticEnabled() {
final ICommandService service = PlatformUI.getWorkbench().getService(ICommandService.class);
final Command command = service.getCommand("toolbox.command.module.translate.automatially");
final State state = command.getState(RegistryToggleState.STATE_ID);
return ((Boolean) state.getValue()).booleanValue();
}
}
org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/handlers/PCalTranslateModuleHandler.java
+ 8
− 97
View file @ 642b540e
......@@ -27,48 +27,21 @@
package org.lamport.tla.toolbox.editor.basic.handlers;
import java.lang.reflect.InvocationTargetException;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
import org.eclipse.core.commands.ExecutionEvent;
import org.eclipse.core.commands.ExecutionException;
import org.eclipse.core.commands.IHandler;
import org.eclipse.core.commands.IHandler2;
import org.eclipse.core.resources.IFile;
import org.eclipse.core.resources.IMarker;
import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.jface.dialogs.ProgressMonitorDialog;
import org.eclipse.jface.operation.IRunnableContext;
import org.eclipse.jface.operation.IRunnableWithProgress;
import org.eclipse.jface.text.BadLocationException;
import org.eclipse.jface.text.FindReplaceDocumentAdapter;
import org.eclipse.jface.text.IDocument;
import org.eclipse.jface.text.IRegion;
import org.eclipse.jface.viewers.ISelection;
import org.eclipse.swt.widgets.Display;
import org.eclipse.ui.IEditorInput;
import org.eclipse.ui.IEditorPart;
import org.eclipse.ui.part.FileEditorInput;
import org.eclipse.ui.handlers.HandlerUtil;
import org.lamport.tla.toolbox.editor.basic.TLAEditor;
import org.lamport.tla.toolbox.editor.basic.TLAEditorAndPDFViewer;
import org.lamport.tla.toolbox.editor.basic.pcal.IPCalReservedWords;
import org.lamport.tla.toolbox.spec.Spec;
import org.lamport.tla.toolbox.tool.ToolboxHandle;
import org.lamport.tla.toolbox.ui.handler.SaveDirtyEditorAbstractHandler;
import org.lamport.tla.toolbox.util.TLAMarkerHelper;
import org.lamport.tla.toolbox.util.UIHelper;
import org.lamport.tla.toolbox.util.pref.IPreferenceConstants;
import org.lamport.tla.toolbox.util.pref.PreferenceStoreHelper;
import pcal.Translator;
import org.lamport.tla.toolbox.editor.basic.pcal.PCalTranslator;
/**
* Triggers the PCal translation of the module
*
* @author Simon Zambrovski
*/
public class PCalTranslateModuleHandler extends SaveDirtyEditorAbstractHandler implements IHandler, IHandler2 {
public class PCalTranslateModuleHandler extends PCalTranslator {
public Object execute(final ExecutionEvent event) throws ExecutionException {
if (!saveDirtyEditor(event)) {
......@@ -76,76 +49,14 @@ public class PCalTranslateModuleHandler extends SaveDirtyEditorAbstractHandler i
return null;
}
final TLAEditor tlaEditor = getTLAEditor(activeEditor);
if (tlaEditor == null) {
// If it's not a TLAEditor, I can't have PlusCal code.
if (tlaEditor == null || !tlaEditor.hasPlusCal()) {
// If it's not a TLAEditor, it can't have PlusCal code.
return null;
}
// Running the PlusCal translator takes too long for the UI thread. Thus, the
// call to the PlusCal translator call is forked off into a non-UI thread.
// However, we use a ProgressMonitorDialog to lock the UI from further
// modifications.
final IRunnableContext context = new ProgressMonitorDialog(Display.getDefault().getActiveShell());
try {
context.run(true, false, new IRunnableWithProgress() {
public void run(final IProgressMonitor progressMonitor) throws InvocationTargetException, InterruptedException {
final IEditorInput editorInput = tlaEditor.getEditorInput();
final IDocument doc = tlaEditor.getDocumentProvider().getDocument(editorInput);
if (editorInput instanceof FileEditorInput && tlaEditor.hasPlusCal()) {
final IFile file = ((FileEditorInput) editorInput).getFile();
final Spec spec = ToolboxHandle.getCurrentSpec();
// Remove all old markers that indicated parser problems in the previous version
// of the editor.
TLAMarkerHelper.removeProblemMarkers(file, progressMonitor,
TLAMarkerHelper.TOOLBOX_MARKERS_TRANSLATOR_MARKER_ID);
// Get the user-defined, per spec translator arguments. In almost all cases this
// is "-nocfg".
final List<String> asList = new ArrayList<String>(
Arrays.asList(PreferenceStoreHelper.getStringArray(spec,
IPreferenceConstants.PCAL_CAL_PARAMS, new String[] { "-nocfg" })));
// Add the name of the current file to the arguments. The Translator expects
// this even though we invoke the translator in a way that it doesn't write files.
asList.add(file.getLocation().toOSString());
// Run the Translator on the input and check if it succeeded. If it didn't
// succeed, we know there are parser problems which we will use to marker the
// editor.
final Translator translator = new Translator(doc.get(), asList);
if (translator.translate()) {
// Update the mapping to/from TLA+ to PlusCal.
spec.setTpMapping(translator.getMapping(), file.getName(), progressMonitor);
if (translator.hasChanged()) {
// Join the UI thread to modify the editor's content.
UIHelper.runUISync(new Runnable() {
public void run() {
// Replace the documents content while preserving the current caret position.
final ISelection selection = tlaEditor.getViewer().getSelection();
doc.set(translator.getOutput());
tlaEditor.getViewer().setSelection(selection);
// Finally save the editor.
tlaEditor.doSave(progressMonitor);
}
});
}
} else {
// Add parser problem markers to the editor.
for (Translator.Error anError : translator.getErrors()) {
TLAMarkerHelper.installProblemMarker(file, file.getName(), IMarker.SEVERITY_ERROR,
anError.getLocation(), anError.toString(), progressMonitor,
TLAMarkerHelper.TOOLBOX_MARKERS_TRANSLATOR_MARKER_ID);
}
}
}
}
});
} catch (InvocationTargetException e) {
throw new ExecutionException(e.getMessage(), e);
} catch (InterruptedException e) {
translate(tlaEditor, HandlerUtil.getActiveShell(event));
} catch (InvocationTargetException | InterruptedException e) {
throw new ExecutionException(e.getMessage(), e);
}
return null;
......
org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/pcal/PCalTranslator.java 0 → 100644
+ 126
− 0
View file @ 642b540e
/*******************************************************************************
* Copyright (c) 2018 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.editor.basic.pcal;
import java.lang.reflect.InvocationTargetException;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
import org.eclipse.core.resources.IFile;
import org.eclipse.core.resources.IMarker;
import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.jface.dialogs.ProgressMonitorDialog;
import org.eclipse.jface.operation.IRunnableContext;
import org.eclipse.jface.operation.IRunnableWithProgress;
import org.eclipse.jface.text.IDocument;
import org.eclipse.jface.viewers.ISelection;
import org.eclipse.swt.widgets.Shell;
import org.eclipse.ui.IEditorInput;
import org.eclipse.ui.part.FileEditorInput;
import org.lamport.tla.toolbox.editor.basic.TLAEditor;
import org.lamport.tla.toolbox.spec.Spec;
import org.lamport.tla.toolbox.tool.ToolboxHandle;
import org.lamport.tla.toolbox.ui.handler.SaveDirtyEditorAbstractHandler;
import org.lamport.tla.toolbox.util.TLAMarkerHelper;
import org.lamport.tla.toolbox.util.UIHelper;
import org.lamport.tla.toolbox.util.pref.IPreferenceConstants;
import org.lamport.tla.toolbox.util.pref.PreferenceStoreHelper;
import pcal.Translator;
public abstract class PCalTranslator extends SaveDirtyEditorAbstractHandler {
protected void translate(final TLAEditor tlaEditor, final Shell shell) throws InvocationTargetException, InterruptedException {
translate(tlaEditor, shell, true);
}
protected void translate(final TLAEditor tlaEditor, final Shell shell, final boolean saveEditor) throws InvocationTargetException, InterruptedException {
// Running the PlusCal translator takes too long for the UI thread. Thus, the
// call to the PlusCal translator call is forked off into a non-UI thread.
// However, we use a ProgressMonitorDialog to lock the UI from further
// modifications.
final IRunnableContext context = new ProgressMonitorDialog(tlaEditor.getEditorSite().getShell());
context.run(true, false, new IRunnableWithProgress() {
public void run(final IProgressMonitor progressMonitor) throws InvocationTargetException, InterruptedException {
final IEditorInput editorInput = tlaEditor.getEditorInput();
final IDocument doc = tlaEditor.getDocumentProvider().getDocument(editorInput);
final IFile file = ((FileEditorInput) editorInput).getFile();
final Spec spec = ToolboxHandle.getCurrentSpec();
// Remove all old markers that indicated parser problems in the previous version
// of the editor.
TLAMarkerHelper.removeProblemMarkers(file, progressMonitor,
TLAMarkerHelper.TOOLBOX_MARKERS_TRANSLATOR_MARKER_ID);
// Get the user-defined, per spec translator arguments. In almost all cases this
// is "-nocfg".
final List<String> asList = new ArrayList<String>(
Arrays.asList(PreferenceStoreHelper.getStringArray(spec,
IPreferenceConstants.PCAL_CAL_PARAMS, new String[] { "-nocfg" })));
// Add the name of the current file to the arguments. The Translator expects
// this even though we invoke the translator in a way that it doesn't write files.
asList.add(file.getLocation().toOSString());
// Run the Translator on the input and check if it succeeded. If it didn't
// succeed, we know there are parser problems which we will use to marker the
// editor.
final Translator translator = new Translator(doc.get(), asList);
if (translator.translate()) {
// Update the mapping to/from TLA+ to PlusCal.
spec.setTpMapping(translator.getMapping(), file.getName(), progressMonitor);
// User might have edited a non-PlusCal part of the editor. In this case, don't
// change the editor to not create a superfluous undo operation.
if (translator.hasChanged()) {
// Join the UI thread to modify the editor's content.
UIHelper.runUISync(new Runnable() {
public void run() {
// Replace the documents content while preserving the current caret position.
final ISelection selection = tlaEditor.getViewer().getSelection();
doc.set(translator.getOutput());
tlaEditor.getViewer().setSelection(selection);
// Finally save the editor.
if (tlaEditor.isDirty() && saveEditor) {
tlaEditor.doSave(progressMonitor);
}
}
});
}
} else {
// Add parser problem markers to the editor.
for (Translator.Error anError : translator.getErrors()) {
TLAMarkerHelper.installProblemMarker(file, file.getName(), IMarker.SEVERITY_ERROR,
anError.getLocation(), anError.toString(), progressMonitor,
TLAMarkerHelper.TOOLBOX_MARKERS_TRANSLATOR_MARKER_ID);
}
}
}
});
}
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment