From 5ce663d8b314065c788c6d9df1cce15c25b3d13d Mon Sep 17 00:00:00 2001 From: Mark Kattenbelt Date: Fri, 31 Oct 2008 12:17:29 +0000 Subject: [PATCH] context menu model editor (potential fix for windows) git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@818 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/model/GUITextModelEditor.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/prism/src/userinterface/model/GUITextModelEditor.java b/prism/src/userinterface/model/GUITextModelEditor.java index aa8b6d18..e6850810 100644 --- a/prism/src/userinterface/model/GUITextModelEditor.java +++ b/prism/src/userinterface/model/GUITextModelEditor.java @@ -235,6 +235,7 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen }; actionCut.putValue(Action.LONG_DESCRIPTION, "Cuts the highlighted text to the clipboard."); actionCut.putValue(Action.NAME, "Cut"); + //actionCut.putValue(Action.ACCELERATOR_KEY, KeyStroke. //actionCut.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("editcut.png")); actionCopy = new AbstractAction() { @@ -270,7 +271,7 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen } } }; - actionUndo.putValue(Action.LONG_DESCRIPTION, "Undos the most recent action."); + actionUndo.putValue(Action.LONG_DESCRIPTION, "Undo the most recent action."); actionUndo.putValue(Action.NAME, "Undo"); actionUndo.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallUndo.png")); @@ -621,7 +622,8 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen * spv */ public void mouseClicked(MouseEvent me) { - + // trying to fix context menu bug under windows. + mousePressed(me); } public void mousePressed(MouseEvent me) {