jump to error when not autoparsing

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@816 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/userinterface/model/GUIModelEditor.java

@@ -50,7 +50,7 @@ public abstract class GUIModelEditor extends JPanel
     
     public abstract void selectAll();
     
-    public void modelParseFailed(PrismLangException parserError) {}
+    public void modelParseFailed(PrismLangException parserError, boolean background) {}
 
     public void modelParseSuccessful() {}
 }

prism/src/userinterface/model/GUIMultiModelHandler.java

@@ -795,11 +795,11 @@ public class GUIMultiModelHandler extends JPanel
         theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODEL_PARSED, parsedModel));
     }
     
-    public synchronized void modelParseFailed(PrismLangException parserError)
+    public synchronized void modelParseFailed(PrismLangException parserError, boolean background)
     {
         lastError = parserError.getMessage();
         
-        editor.modelParseFailed(parserError);
+        editor.modelParseFailed(parserError, background);
         
         tree.stopParsing();
         parsing = false;
@@ -903,7 +903,7 @@ public class GUIMultiModelHandler extends JPanel
     
     public synchronized void modelBuildFailed(PrismException e)
     {
-    	if (e != null && e instanceof PrismLangException) editor.modelParseFailed((PrismLangException)e);
+    	if (e != null && e instanceof PrismLangException) editor.modelParseFailed((PrismLangException)e, false);
         
         if(exportAfterReceiveBuildNotification)
         {

prism/src/userinterface/model/GUITextModelEditor.java

@@ -297,9 +297,9 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen
 		// search and replace action
         actionSearch = new AbstractAction() {
         	public void actionPerformed(ActionEvent ae) {
-        		
+        		/*
         		// System.out.println("search button pressed");
-        		/*	if (GUIMultiModelHandler.isDoingSearch()) {
+        		if (GUIMultiModelHandler.isDoingSearch()) {
 					
 				} else {
 					try {
@@ -309,13 +309,14 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen
 						GUIPrism.getGUI().getMultiLogger().logMessage(prism.log.PrismLogLevel.PRISM_ERROR,
 								pnfe.getMessage());
 					}
-				}*/
+				}
+				*/
         	}
         };
         actionSearch.putValue(Action.LONG_DESCRIPTION, "Opens a find and replace dialog.");
         //actionSearch.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("find.png"));
         actionSearch.putValue(Action.NAME, "Find/Replace");
-        //actionSearch.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_F, InputEvent.CTRL_MASK));
+        //actionSearch.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_R, InputEvent.CTRL_MASK));
         
         insertDTMC = new AbstractAction() {
         	public void actionPerformed(ActionEvent ae) {
@@ -664,6 +665,21 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen
 		
 	}
 	
+	public void jumpToError()
+	{
+		if (parseError != null && parseError.hasLineNumbers() )
+		{
+			try
+			{
+				editor.setCaretPosition(computeDocumentOffset(parseError.getBeginLine(), parseError.getBeginColumn()));
+			}
+			catch (BadLocationException e)
+			{
+				
+			}
+		}
+	}
+	
 	public void refreshErrorDisplay()
 	{
 		if (parseErrorHighlightKey != null)
@@ -675,13 +691,18 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen
 		if (parseError != null && parseError.hasLineNumbers() )
 		{
 			String error = parseError.getMessage();
+		
+			// Just the first line.
+			errorLines.put(parseError.getBeginLine(), error);
 			
-			for (int line = parseError.getBeginLine();
+			// If error spans multiple lines, this code will put
+			// an error in every line of the gutter.
+			/*for (int line = parseError.getBeginLine();
 			     line <= parseError.getEndLine();
 			     line++)
 			{
 				errorLines.put(line, error);
-			}
+			}*/
 		}
 		
 		gutter.setParseErrors(errorLines);
@@ -699,10 +720,8 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen
 			catch (BadLocationException e)
 			{
 				
-			}
-			
-		}
-		
+			}			
+		}		
 	}
 	
 	public int computeDocumentOffset(int line, int column) throws BadLocationException
@@ -737,16 +756,19 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen
 		return beginLineOffset+documentChar;		
 	}
 	
-	public void modelParseFailed(PrismLangException parserError) 
+	public void modelParseFailed(PrismLangException parserError, boolean background) 
 	{	
 		this.parseError = parserError;		
-		refreshErrorDisplay();
+		refreshErrorDisplay();	
+		if (!background)
+			jumpToError();		
 	}
 
 	@Override
 	public void modelParseSuccessful() 
 	{
 		this.parseError = null;
+		// get rid of any error highlighting
 		refreshErrorDisplay();
 	} 
 	

prism/src/userinterface/model/computation/BuildModelThread.java

@@ -109,7 +109,7 @@ public class BuildModelThread extends GUIComputationThread
 					plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_ERROR, plug));
 					plug.setTaskBarText("Parsing model... error.");
 					error(parseError.getMessage());
-					handler.modelParseFailed(parseError);
+					handler.modelParseFailed(parseError, false);
 					handler.modelBuildFailed(null);
 				}});
 				return;

prism/src/userinterface/model/computation/ParseModelThread.java

@@ -97,7 +97,7 @@ public class ParseModelThread extends GUIComputationThread
 					plug.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_ERROR, plug));
 					if(!background) plug.setTaskBarText("Parsing model... error.");
 					if(!background) error(errMsg);
-					handler.modelParseFailed(parseError);			
+					handler.modelParseFailed(parseError, background);			
 				}
 			});
 			return;