diff --git a/prism/src/userinterface/model/GUIModelEditor.java b/prism/src/userinterface/model/GUIModelEditor.java index a0865125..4f6a10b9 100644 --- a/prism/src/userinterface/model/GUIModelEditor.java +++ b/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() {} } diff --git a/prism/src/userinterface/model/GUIMultiModelHandler.java b/prism/src/userinterface/model/GUIMultiModelHandler.java index c0fdf143..c54c5f24 100644 --- a/prism/src/userinterface/model/GUIMultiModelHandler.java +++ b/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) { diff --git a/prism/src/userinterface/model/GUITextModelEditor.java b/prism/src/userinterface/model/GUITextModelEditor.java index 05e30cca..99c1fe39 100644 --- a/prism/src/userinterface/model/GUITextModelEditor.java +++ b/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(); } diff --git a/prism/src/userinterface/model/computation/BuildModelThread.java b/prism/src/userinterface/model/computation/BuildModelThread.java index b3d3860a..a29354fa 100644 --- a/prism/src/userinterface/model/computation/BuildModelThread.java +++ b/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; diff --git a/prism/src/userinterface/model/computation/ParseModelThread.java b/prism/src/userinterface/model/computation/ParseModelThread.java index 6dc58491..b237e4b0 100644 --- a/prism/src/userinterface/model/computation/ParseModelThread.java +++ b/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;