Error Marker wird wieder gesetzt.

This commit is contained in:
Michael Uhl 2019-04-28 20:42:04 +02:00
parent 9acf2c0ed5
commit 8df6de3228

View File

@ -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()))));
}
});