From 5587e0c16f87db19f65bd206fa9cf7ecec2c8a93 Mon Sep 17 00:00:00 2001
From: Mark Kattenbelt <mark.kattenbelt@comlab.ox.ac.uk>
Date: Mon, 3 Nov 2008 15:31:12 +0000
Subject: [PATCH] fixed model context menu bug in windows

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@822 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 .../model/GUITextModelEditor.java             | 49 ++++---------------
 1 file changed, 10 insertions(+), 39 deletions(-)

diff --git a/prism/src/userinterface/model/GUITextModelEditor.java b/prism/src/userinterface/model/GUITextModelEditor.java
index 12baa6bc..3078aeed 100644
--- a/prism/src/userinterface/model/GUITextModelEditor.java
+++ b/prism/src/userinterface/model/GUITextModelEditor.java
@@ -626,54 +626,25 @@ 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) {
-		
+	public void mouseTriggered(MouseEvent me)
+	{
 		if (me.isPopupTrigger()) {
-			/*
-			
-			// check if to have paste enabled or not
-			Clipboard clipboard = Toolkit.getDefaultToolkit().getSystemClipboard();
-			if (clipboard.getContents(null) != null) {
-				actionPaste.setEnabled(false);
-			}			
-			else {
-				actionPaste.setEnabled(true);
-			}
-			
-			// check if text highlighted or not
-			if (editor.getSelectedText() == null) {
-				actionCut.setEnabled(false);
-				actionCopy.setEnabled(false);
-			}
-			else {
-				actionCut.setEnabled(true);
-				actionCopy.setEnabled(true);
-			}
-			*/
-			// check undo
-			
-			//GUIPrism.getClipboardPlugin().getUndoAction().setEnabled(undoManager.canUndo());
-			//GUIPrism.getClipboardPlugin().getRedoAction().setEnabled(undoManager.canRedo());
-						
 			actionJumpToError.setEnabled(parseError != null && parseError.hasLineNumbers());
 			((GUIMultiModel)handler.getGUIPlugin()).doEnables();
 			
 			contextPopup.show(me.getComponent(), me.getX(), me.getY());
 			
 		}
+	} 
+	 
+	public void mouseClicked(MouseEvent me) {}
+	public void mousePressed(MouseEvent me) {
+		mouseTriggered(me);		
 	}
-	public void mouseEntered(MouseEvent me) {
-		
-	}
-	public void mouseExited(MouseEvent me) {
-		
-	}
+	public void mouseEntered(MouseEvent me) {}
+	public void mouseExited(MouseEvent me) {}
 	public void mouseReleased(MouseEvent me) {
-		
+		mouseTriggered(me);	
 	}
 	
 	public void jumpToError()