From 277ca2d17a90cf4bff82f2051f5f14bc116f6aac Mon Sep 17 00:00:00 2001 From: Mark Kattenbelt Date: Fri, 31 Oct 2008 11:42:47 +0000 Subject: [PATCH] added context menu option to jump to error git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@817 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../model/GUITextModelEditor.java | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/prism/src/userinterface/model/GUITextModelEditor.java b/prism/src/userinterface/model/GUITextModelEditor.java index 99c1fe39..aa8b6d18 100644 --- a/prism/src/userinterface/model/GUITextModelEditor.java +++ b/prism/src/userinterface/model/GUITextModelEditor.java @@ -82,7 +82,7 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen private JPopupMenu contextPopup; /** Actions for the context menu. */ - private Action actionCut, actionCopy, actionPaste, actionUndo, actionRedo, actionSearch; + private Action actionCut, actionCopy, actionPaste, actionUndo, actionRedo, actionSearch, actionJumpToError; /** More actions */ private Action insertDTMC, insertCTMC, insertMDP; @@ -289,10 +289,21 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen } } }; + + actionRedo.putValue(Action.LONG_DESCRIPTION, "Redos the most recent undo"); actionRedo.putValue(Action.NAME, "Redo"); actionRedo.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallRedo.png")); + actionJumpToError = new AbstractAction() { + public void actionPerformed(ActionEvent ae) { + jumpToError(); + } + }; + + actionJumpToError.putValue(Action.NAME, "Jump to error"); + actionJumpToError.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("tinyError.png")); + // search and replace action actionSearch = new AbstractAction() { @@ -389,7 +400,8 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen contextPopup.add(actionCopy); contextPopup.add(actionPaste); contextPopup.add(new JSeparator()); - contextPopup.add(actionSearch); + contextPopup.add(actionJumpToError); + //contextPopup.add(actionSearch); if (editor.getContentType().equals("text/prism")) @@ -651,6 +663,8 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen actionRedo.setEnabled(false); } + actionJumpToError.setEnabled(parseError != null && parseError.hasLineNumbers()); + contextPopup.show(me.getComponent(), me.getX(), me.getY()); }