ModelEditor shows stale errors.

[Bug][Toolbox]

org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/ModelEditor.java

@@ -127,6 +127,21 @@ public class ModelEditor extends FormEditor
 									TLCUIActivator.getDefault().logError("Error initializing editor", e);
 								}
 							}
+							
+							// MAK 01/2018: Re-validate the page because running the model removes or sets
+							// problem markers (Model#setMarkers) which are presented to the user by
+							// ModelEditor#handleProblemMarkers. If we don't re-validate once a model is
+							// done running, the user visible presentation resulting from an earlier run of
+							// handleProblemMarkers gets stale.
+							// This behavior can be triggered by creating a spec (note commented EXTENDS): 
+							//   \* EXTENDS Integers
+							//   VARIABLE s
+							//   Spec == s = 0 /\ [][s'=s]_s
+							// and a model that defines the invariant (s >= 0). Upon the first launch of
+							// the model, the ModelEditor correctly marks the invariant due to the operator
+							// >= being not defined. Uncommenting EXTENDS, saving the spec and rerunning
+							// the model would incorrectly not remove the marker on the invariant.
+							UIHelper.runUISync(validateRunable);
 						}
 					}
 				});

org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/BasicFormPage.java

@@ -458,7 +458,7 @@ public abstract class BasicFormPage extends FormPage implements IModelConfigurat
     /**
      * Handle the problem markers 
      */
-    public void handleProblemMarkers(boolean switchToErrorPage)
+    private void handleProblemMarkers(boolean switchToErrorPage)
     {
         // delegate to the editor
         ((ModelEditor) getEditor()).handleProblemMarkers(switchToErrorPage);

org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java

@@ -523,7 +523,7 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate implemen
         // parse the MC file
         IParseResult parseResult = ToolboxHandle.parseModule(rootModule, new SubProgressMonitor(monitor, 1), false,
                 false);
-        Vector<TLAMarkerInformationHolder> detectedErrors = parseResult.getDetectedErrors();
+        final Vector<TLAMarkerInformationHolder> detectedErrors = parseResult.getDetectedErrors();
         boolean status = !AdapterFactory.isProblemStatus(parseResult.getStatus());
 
         monitor.worked(1);