Skip to content
Snippets Groups Projects
Commit 0adb16ef authored by Jens Bendisposto's avatar Jens Bendisposto
Browse files

add context/machine name to rodinpos

parent 4b9da9f5
No related branches found
No related tags found
No related merge requests found
...@@ -22,4 +22,6 @@ public abstract class AbstractComponentTranslator { ...@@ -22,4 +22,6 @@ public abstract class AbstractComponentTranslator {
return Collections.unmodifiableMap(labelMapping); return Collections.unmodifiableMap(labelMapping);
} }
abstract public String getResource();
} }
\ No newline at end of file
...@@ -11,6 +11,7 @@ import java.util.Collection; ...@@ -11,6 +11,7 @@ import java.util.Collection;
import java.util.Map; import java.util.Map;
import org.eclipse.core.runtime.Assert; import org.eclipse.core.runtime.Assert;
import org.eventb.core.IEvent;
import org.eventb.core.IEventBProject; import org.eventb.core.IEventBProject;
import org.eventb.core.IEventBRoot; import org.eventb.core.IEventBRoot;
import org.eventb.core.ISCInternalContext; import org.eventb.core.ISCInternalContext;
...@@ -52,7 +53,7 @@ public abstract class EventBTranslator implements ITranslator { ...@@ -52,7 +53,7 @@ public abstract class EventBTranslator implements ITranslator {
for (AbstractComponentTranslator t : translators) { for (AbstractComponentTranslator t : translators) {
final Map<Node, IInternalElement> labelMapping = t final Map<Node, IInternalElement> labelMapping = t
.getLabelMapping(); .getLabelMapping();
printer.addNodes(labelMapping); printer.addNodes(labelMapping, t.getResource());
} }
return printer; return printer;
} }
......
...@@ -35,15 +35,15 @@ public class LabelPositionPrinter implements PositionPrinter { ...@@ -35,15 +35,15 @@ public class LabelPositionPrinter implements PositionPrinter {
private final Map<Node, NodeInfo> nodeInfos = new ConcurrentHashMap<Node, NodeInfo>(); private final Map<Node, NodeInfo> nodeInfos = new ConcurrentHashMap<Node, NodeInfo>();
public void addNode(final Node node, final IInternalElement element) public void addNode(final Node node, final IInternalElement element,
throws TranslationFailedException { String file) throws TranslationFailedException {
final String label, source; final String label, source;
try { try {
if (element instanceof ITraceableElement) { if (element instanceof ITraceableElement) {
// get name of unchecked element // get name of unchecked element
IRodinElement traceableSource; IRodinElement traceableSource;
traceableSource = ((ITraceableElement) element).getSource(); traceableSource = ((ITraceableElement) element).getSource();
source = traceableSource.getElementName(); source = traceableSource.getElementName();
} else { } else {
source = null; source = null;
...@@ -53,7 +53,8 @@ public class LabelPositionPrinter implements PositionPrinter { ...@@ -53,7 +53,8 @@ public class LabelPositionPrinter implements PositionPrinter {
} else { } else {
label = null; label = null;
} }
addNode(node, label, source);
addNode(node, label, source, file);
} catch (RodinDBException e) { } catch (RodinDBException e) {
final String message = "A Rodin exception occured during translation process, you can try to fix that by cleaning the project. Original Exception: "; final String message = "A Rodin exception occured during translation process, you can try to fix that by cleaning the project. Original Exception: ";
throw new TranslationFailedException(element.getElementName(), throw new TranslationFailedException(element.getElementName(),
...@@ -61,19 +62,19 @@ public class LabelPositionPrinter implements PositionPrinter { ...@@ -61,19 +62,19 @@ public class LabelPositionPrinter implements PositionPrinter {
} }
} }
public void addNodes(final Map<Node, IInternalElement> nodeMapping) public void addNodes(final Map<Node, IInternalElement> nodeMapping,
throws TranslationFailedException { String name) throws TranslationFailedException {
for (Entry<Node, IInternalElement> item : nodeMapping.entrySet()) { for (Entry<Node, IInternalElement> item : nodeMapping.entrySet()) {
final Node key = item.getKey(); final Node key = item.getKey();
final IInternalElement value = item.getValue(); final IInternalElement value = item.getValue();
addNode(key, value); addNode(key, value, name);
} }
} }
private void addNode(final Node node, final String label, private void addNode(final Node node, final String label,
final String elementName) { final String elementName, String file) {
if (label != null || elementName != null) { if (label != null || elementName != null) {
nodeInfos.put(node, new NodeInfo(label, elementName)); nodeInfos.put(node, new NodeInfo(label, elementName, file));
} }
} }
...@@ -83,6 +84,11 @@ public class LabelPositionPrinter implements PositionPrinter { ...@@ -83,6 +84,11 @@ public class LabelPositionPrinter implements PositionPrinter {
pout.printAtom("none"); pout.printAtom("none");
} else { } else {
pout.openTerm("rodinpos"); pout.openTerm("rodinpos");
if (info.file == null) {
pout.emptyList();
} else {
pout.printAtom(info.file);
}
if (info.label == null) { if (info.label == null) {
pout.emptyList(); pout.emptyList();
} else { } else {
...@@ -104,11 +110,14 @@ public class LabelPositionPrinter implements PositionPrinter { ...@@ -104,11 +110,14 @@ public class LabelPositionPrinter implements PositionPrinter {
private static class NodeInfo { private static class NodeInfo {
private final String label; private final String label;
private final String elementName; private final String elementName;
private final String file;
public NodeInfo(final String label, final String elementName) { public NodeInfo(final String label, final String elementName,
String file) {
super(); super();
this.label = label; this.label = label;
this.elementName = elementName; this.elementName = elementName;
this.file = file;
} }
} }
......
...@@ -35,7 +35,6 @@ import org.eventb.core.ISCRefinesMachine; ...@@ -35,7 +35,6 @@ import org.eventb.core.ISCRefinesMachine;
import org.eventb.core.ISCVariable; import org.eventb.core.ISCVariable;
import org.eventb.core.ISCVariant; import org.eventb.core.ISCVariant;
import org.eventb.core.ISCWitness; import org.eventb.core.ISCWitness;
import org.eventb.core.ITheorem;
import org.eventb.core.ITraceableElement; import org.eventb.core.ITraceableElement;
import org.eventb.core.ast.FormulaFactory; import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment; import org.eventb.core.ast.ITypeEnvironment;
...@@ -528,4 +527,9 @@ public class ModelTranslator extends AbstractComponentTranslator { ...@@ -528,4 +527,9 @@ public class ModelTranslator extends AbstractComponentTranslator {
return result; return result;
} }
@Override
public String getResource() {
return machine.getComponentName();
}
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment