From 8df6de3228052219971b9957e62efc6f745306ba Mon Sep 17 00:00:00 2001 From: Michael Uhl Date: Sun, 28 Apr 2019 20:42:04 +0200 Subject: [PATCH] Error Marker wird wieder gesetzt. --- .../src/typinferenzplugin/editor/JavEditor.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/JavaCompilerPlugin/bundles/JavaCompilerPlugin.Plugin/src/typinferenzplugin/editor/JavEditor.java b/JavaCompilerPlugin/bundles/JavaCompilerPlugin.Plugin/src/typinferenzplugin/editor/JavEditor.java index 612611f..a01307f 100644 --- a/JavaCompilerPlugin/bundles/JavaCompilerPlugin.Plugin/src/typinferenzplugin/editor/JavEditor.java +++ b/JavaCompilerPlugin/bundles/JavaCompilerPlugin.Plugin/src/typinferenzplugin/editor/JavEditor.java @@ -2,8 +2,10 @@ package typinferenzplugin.editor; import static org.eclipse.core.runtime.IStatus.ERROR; import static typinferenzplugin.Activator.PLUGIN_ID; +import static java.util.Collections.singletonList; import java.util.Collection; +import java.util.Collections; import java.util.TreeSet; import java.util.Vector; @@ -131,7 +133,8 @@ public class JavEditor extends TextEditor implements UnifyResultListener { try { typeinference.run(this); } catch (TypeinferenceException texc) { - markers.add(new ErrorMarker(texc.getMessage(), new CodePoint(texc.getOffset()))); + //markers.add(new ErrorMarker(texc.getMessage(), new CodePoint(texc.getOffset()))); + this.placeMarkers(extractResource(), singletonList(new ErrorMarker(texc.getMessage(), new CodePoint(texc.getOffset())))); } });