From 5853d638c0252771a83c6bc434b59249e3fe5fa7 Mon Sep 17 00:00:00 2001 From: Mark Kattenbelt Date: Thu, 22 Oct 2009 11:55:07 +0000 Subject: [PATCH] bugfix copy/paste git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1540 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/log/GUILog.java | 2 +- prism/src/userinterface/model/GUIMultiModel.java | 2 +- prism/src/userinterface/properties/GUIMultiProperties.java | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/prism/src/userinterface/log/GUILog.java b/prism/src/userinterface/log/GUILog.java index 18b0ac27..8aa5bbbd 100644 --- a/prism/src/userinterface/log/GUILog.java +++ b/prism/src/userinterface/log/GUILog.java @@ -125,7 +125,7 @@ public class GUILog extends GUIPlugin implements MouseListener, PrismSettingsLis theLog.print(le.getData()); } } - else if (e instanceof GUIClipboardEvent) + else if (e instanceof GUIClipboardEvent && super.getGUI().getFocussedPlugin() == this) { GUIClipboardEvent ce = (GUIClipboardEvent)e; if(ce.getID() == GUIClipboardEvent.COPY) diff --git a/prism/src/userinterface/model/GUIMultiModel.java b/prism/src/userinterface/model/GUIMultiModel.java index 4b446224..a27c537b 100644 --- a/prism/src/userinterface/model/GUIMultiModel.java +++ b/prism/src/userinterface/model/GUIMultiModel.java @@ -744,7 +744,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener handler.requestParse(false); } } - else if(e instanceof GUIClipboardEvent) + else if(e instanceof GUIClipboardEvent && super.getGUI().getFocussedPlugin() == this) { GUIClipboardEvent ce = (GUIClipboardEvent)e; if(ce.getComponent() == this) diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 60438d01..c44d446c 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -1155,7 +1155,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List setComputing(false); } } - else if(e instanceof GUIClipboardEvent) + else if(e instanceof GUIClipboardEvent && super.getGUI().getFocussedPlugin() == this) { GUIClipboardEvent ce = (GUIClipboardEvent)e;