Don't delete error messages when calling pushtoUIThread multiple times.

CupPlugin/src/de/tum/in/www2/cupplugin/controller/DocumentDidChangeJob.java

@@ -105,10 +105,10 @@ public class DocumentDidChangeJob extends Job {
 		if (document == null)
 			return Status.CANCEL_STATUS;
 
-
 		IFile file = ((FileEditorInput) myEditor.getEditorInput()).getFile();
-		CupEditorErrorReporter errorReporter = new CupEditorErrorReporter(file);
-
+		CupEditorErrorReporter errorReporter = new CupEditorErrorReporter(file);		
+		errorReporter.resetOnNextPush();
+		
 		CupParser parser = null;
 		
 		if (jobs.contains(JobsToDo.parseCode)) {

CupPlugin/src/de/tum/in/www2/cupplugin/editors/CupEditorErrorReporter.java

@@ -31,14 +31,22 @@ public class CupEditorErrorReporter implements IErrorReporter {
 
 	private IFile file;
 	private List<BufferedMessage> lst = new ArrayList<BufferedMessage>();
+	private boolean doResetErrors;
 
 	public CupEditorErrorReporter(IFile file) {
 		this.file = file;
 	}
 
+	public void resetOnNextPush() {
+		doResetErrors = true;
+	}
+
 	public void pushToUIThread() {
 		List<BufferedMessage> copy;
 		
+		boolean reset = doResetErrors;
+		doResetErrors = false;
+		
 		if (lst.size() < MAX_DISPLAYED_ERRORS) {
 			copy = new ArrayList<BufferedMessage>(lst);
 		} else {
@@ -59,18 +67,22 @@ public class CupEditorErrorReporter implements IErrorReporter {
 		
 		lst.clear();
 
-
 		Display.getDefault().asyncExec(new Runnable() {
 		  public void run() {
-
-			IMarker[] oldMarkers;
-			try {
-				oldMarkers = file.findMarkers(CUP_MARKER, false, 10);
-				for (IMarker m : oldMarkers)
-					m.delete();
-			} catch (CoreException e) {
-				// TODO Auto-generated catch block
-				e.printStackTrace();
+			  
+			// TODO: this only works if we can make sure that asyncExec 
+			//       calls are sequential, future pushToUIThread calls 
+			//       don't add messages that are deleted here.
+			if (reset) {
+				IMarker[] oldMarkers;
+				try {
+					oldMarkers = file.findMarkers(CUP_MARKER, false, 10);
+					for (IMarker m : oldMarkers)
+						m.delete();
+				} catch (CoreException e) {
+					// TODO Auto-generated catch block
+					e.printStackTrace();
+				}
 			}
 			
 			for (BufferedMessage msg : copy) {