From 683a4c53e74b716a834eccdfd60de2bebc1cae54 Mon Sep 17 00:00:00 2001 From: Mark Kattenbelt Date: Fri, 3 Nov 2006 16:30:03 +0000 Subject: [PATCH] Updated the copy/paste mechanism such that properties are actually put on the clipboard as objects (GUIClipboardProperties). This fixes some bugs with regards to copy/pasting properties. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@117 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/GUIClipboard.java | 141 ++++++++++++------ .../properties/GUIMultiProperties.java | 113 ++++++++++++-- .../properties/GUIPropertiesList.java | 48 +++--- .../userinterface/properties/GUIProperty.java | 3 +- 4 files changed, 211 insertions(+), 94 deletions(-) diff --git a/prism/src/userinterface/GUIClipboard.java b/prism/src/userinterface/GUIClipboard.java index 0fd00a11..50a9808b 100644 --- a/prism/src/userinterface/GUIClipboard.java +++ b/prism/src/userinterface/GUIClipboard.java @@ -33,7 +33,9 @@ public class GUIClipboard extends GUIPlugin { private JMenu editMenu; private JToolBar editToolBar; - private Action actionCut, actionCopy, actionPaste, actionDelete, actionSelectAll; + private Action menuActionCut, menuActionCopy, menuActionPaste, menuActionDelete, menuActionSelectAll; + private Action toolbarActionCut, toolbarActionCopy, toolbarActionPaste, toolbarActionDelete, toolbarActionSelectAll; + /** Creates a new instance of GUIClipboard */ public GUIClipboard(GUIPrism pr) @@ -91,25 +93,25 @@ public class GUIClipboard extends GUIPlugin editMenu = new javax.swing.JMenu(); { JMenuItem cut = new javax.swing.JMenuItem(); - cut.setAction(actionCut); + cut.setAction(menuActionCut); cut.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_X, InputEvent.CTRL_MASK)); JMenuItem copy = new javax.swing.JMenuItem(); - copy.setAction(actionCopy); + copy.setAction(menuActionCopy); copy.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_C, InputEvent.CTRL_MASK)); JMenuItem paste = new javax.swing.JMenuItem(); - paste.setAction(actionPaste); + paste.setAction(menuActionPaste); paste.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_V, InputEvent.CTRL_MASK)); JMenuItem delete = new javax.swing.JMenuItem(); - delete.setAction(actionDelete); + delete.setAction(menuActionDelete); delete.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_D, InputEvent.CTRL_MASK)); JSeparator jSeparator3 = new javax.swing.JSeparator(); JMenuItem selectAll = new javax.swing.JMenuItem(); - selectAll.setAction(actionSelectAll); + selectAll.setAction(menuActionSelectAll); selectAll.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_A, InputEvent.CTRL_MASK)); editMenu.setMnemonic(KeyEvent.VK_E); @@ -124,23 +126,23 @@ public class GUIClipboard extends GUIPlugin editToolBar = new JToolBar(); { - JButton b1 = new JButton(actionCut); + JButton b1 = new JButton(toolbarActionCut); b1.setToolTipText("Cut"); b1.setText(""); editToolBar.add(b1); - JButton b2 = new JButton(actionCopy); + JButton b2 = new JButton(toolbarActionCopy); b2.setToolTipText("Copy"); b2.setText(""); editToolBar.add(b2); - JButton b3 = new JButton(actionPaste); + JButton b3 = new JButton(toolbarActionPaste); b3.setToolTipText("Paste"); b3.setText(""); editToolBar.add(b3); - JButton b4 = new JButton(actionDelete); + JButton b4 = new JButton(toolbarActionDelete); b4.setToolTipText("Delete"); b4.setText(""); editToolBar.add(b4); @@ -150,76 +152,123 @@ public class GUIClipboard extends GUIPlugin private void setupActions() { - actionCut = new AbstractAction() + menuActionCut = new AbstractAction() { public void actionPerformed(ActionEvent e) { - //System.out.println("cutactionperforemd"); - //System.out.println("cut"); notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.CUT, getFocussedComponent())); } }; - actionCut.putValue(Action.LONG_DESCRIPTION, "Copys the currently selected item/text to the clipboard and then removes it."); + menuActionCut.putValue(Action.LONG_DESCRIPTION, "Copys the currently selected item/text to the clipboard and then removes it."); //actionCut.putValue(Action.SHORT_DESCRIPTION, "Cut"); - actionCut.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_C)); - actionCut.putValue(Action.NAME, "Cut"); - actionCut.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallCut.gif")); + menuActionCut.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_C)); + menuActionCut.putValue(Action.NAME, "Cut"); + menuActionCut.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallCut.gif")); + + toolbarActionCut = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.CUT, getFocussedComponent())); + } + }; + toolbarActionCut.putValue(Action.LONG_DESCRIPTION, "Copys the currently selected item/text to the clipboard and then removes it."); + toolbarActionCut.putValue(Action.NAME, "Cut"); + toolbarActionCut.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallCut.gif")); + + - actionCopy = new AbstractAction() + menuActionCopy = new AbstractAction() { public void actionPerformed(ActionEvent e) { - //System.out.println("copyactionperforemd"); - //System.out.println("copy"); - notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.COPY, getFocussedComponent())); + notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.COPY, getFocussedComponent())); } }; - actionCopy.putValue(Action.LONG_DESCRIPTION, "Copys the currently selected item/text to the clipboard."); - //actionCopy.putValue(Action.SHORT_DESCRIPTION, "Copy"); - actionCopy.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_O)); - actionCopy.putValue(Action.NAME, "Copy"); - actionCopy.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallCopy.gif")); + menuActionCopy.putValue(Action.LONG_DESCRIPTION, "Copys the currently selected item/text to the clipboard."); + menuActionCopy.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_O)); + menuActionCopy.putValue(Action.NAME, "Copy"); + menuActionCopy.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallCopy.gif")); - actionPaste = new AbstractAction() + toolbarActionCopy = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.COPY, getFocussedComponent())); + } + }; + toolbarActionCopy.putValue(Action.LONG_DESCRIPTION, "Copys the currently selected item/text to the clipboard."); + toolbarActionCopy.putValue(Action.NAME, "Copy"); + toolbarActionCopy.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallCopy.gif")); + + menuActionPaste = new AbstractAction() { public void actionPerformed(ActionEvent e) { - //System.out.println("pasteactionperofemd"); - //System.out.println("paste"); notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.PASTE, getFocussedComponent())); } }; - actionPaste.putValue(Action.LONG_DESCRIPTION, "Pastes the contents of the clipboard."); - //actionPaste.putValue(Action.SHORT_DESCRIPTION, "Paste"); - actionPaste.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_P)); - actionPaste.putValue(Action.NAME, "Paste"); - actionPaste.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallPaste.gif")); + menuActionPaste.putValue(Action.LONG_DESCRIPTION, "Pastes the contents of the clipboard."); + menuActionPaste.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_P)); + menuActionPaste.putValue(Action.NAME, "Paste"); + menuActionPaste.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallPaste.gif")); - actionDelete = new AbstractAction() + toolbarActionPaste = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.PASTE, getFocussedComponent())); + } + }; + toolbarActionPaste.putValue(Action.LONG_DESCRIPTION, "Pastes the contents of the clipboard."); + toolbarActionPaste.putValue(Action.NAME, "Paste"); + toolbarActionPaste.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallPaste.gif")); + + menuActionDelete = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.DELETE, getFocussedComponent())); + } + }; + menuActionDelete.putValue(Action.LONG_DESCRIPTION, "Removes the currently selected item"); + menuActionDelete.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_D)); + menuActionDelete.putValue(Action.NAME, "Delete"); + menuActionDelete.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallDelete.gif")); + + toolbarActionDelete = new AbstractAction() { public void actionPerformed(ActionEvent e) { notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.DELETE, getFocussedComponent())); } }; - actionDelete.putValue(Action.LONG_DESCRIPTION, "Removes the currently selected item"); - //actionDelete.putValue(Action.SHORT_DESCRIPTION, "Delete"); - actionDelete.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_D)); - actionDelete.putValue(Action.NAME, "Delete"); - actionDelete.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallDelete.gif")); + toolbarActionDelete.putValue(Action.LONG_DESCRIPTION, "Removes the currently selected item"); + toolbarActionDelete.putValue(Action.NAME, "Delete"); + toolbarActionDelete.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallDelete.gif")); + + menuActionSelectAll = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.SELECT_ALL, getFocussedComponent())); + } + }; + menuActionSelectAll.putValue(Action.LONG_DESCRIPTION, "Selects all items of the focussed component."); + menuActionSelectAll.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_S)); + menuActionSelectAll.putValue(Action.NAME, "Select all"); + menuActionSelectAll.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallSelectAll.gif")); - actionSelectAll = new AbstractAction() + toolbarActionSelectAll = new AbstractAction() { public void actionPerformed(ActionEvent e) { notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.SELECT_ALL, getFocussedComponent())); } }; - actionSelectAll.putValue(Action.LONG_DESCRIPTION, "Selects all items of the focussed component."); - //actionSelectAll.putValue(Action.SHORT_DESCRIPTION, "Select All"); - actionSelectAll.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_S)); - actionSelectAll.putValue(Action.NAME, "Select all"); - actionSelectAll.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallSelectAll.gif")); + toolbarActionSelectAll.putValue(Action.LONG_DESCRIPTION, "Selects all items of the focussed component."); + toolbarActionSelectAll.putValue(Action.NAME, "Select all"); + toolbarActionSelectAll.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallSelectAll.gif")); } public OptionsPanel getOptions() diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 29dcf206..de61fcb2 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -1,6 +1,6 @@ //============================================================================== // -// Copyright (c) 2002-2005, Andrew Hinton, Dave Parker +// Copyright (c) 2002-2006, Andrew Hinton, Dave Parker, Mark Kattenbelt // // This file is part of PRISM. // @@ -36,7 +36,7 @@ import java.util.*; import userinterface.util.*; import userinterface.simulator.*; import userinterface.simulator.networking.*; - +import java.awt.datatransfer.*; /** * Properties panel designed to handle constants as well as properties. * Also designed to handle experiments. @@ -888,34 +888,51 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List public void a_cut() { java.awt.datatransfer.Clipboard clipboard = Toolkit.getDefaultToolkit().getSystemClipboard(); - java.awt.datatransfer.StringSelection selection = new java.awt.datatransfer.StringSelection(propList.getClipboardString()); - clipboard.setContents(selection, null); + //java.awt.datatransfer.StringSelection selection = new java.awt.datatransfer.StringSelection(propList.getClipboardString()); + //clipboard.setContents(selection, null); + clipboard.setContents(new GUIClipboardProperties(propList.getSelectedProperties()), null); a_delete(); } public void a_copy() { java.awt.datatransfer.Clipboard clipboard = Toolkit.getDefaultToolkit().getSystemClipboard(); - java.awt.datatransfer.StringSelection selection = new java.awt.datatransfer.StringSelection(propList.getClipboardString()); - clipboard.setContents(selection, null); + //java.awt.datatransfer.StringSelection selection = new java.awt.datatransfer.StringSelection(propList.getClipboardString()); + //clipboard.setContents(selection, null); + clipboard.setContents(new GUIClipboardProperties(propList.getSelectedProperties()), null); } public void a_paste() { - java.awt.datatransfer.Clipboard clipboard = Toolkit.getDefaultToolkit().getSystemClipboard(); - java.awt.datatransfer.Transferable contents = clipboard.getContents(null); + Clipboard clipboard = Toolkit.getDefaultToolkit().getSystemClipboard(); + Transferable contents = clipboard.getContents(null); + if(contents !=null) { - try - { - String text = (String)contents.getTransferData(java.awt.datatransfer.DataFlavor.stringFlavor); - propList.pastePropertiesString(text); - } - catch(java.awt.datatransfer.UnsupportedFlavorException e) + if (contents.isDataFlavorSupported(getGUIClipboardPropertiesDataFlavor())) { + try + { + GUIClipboardProperties gcp = (GUIClipboardProperties)contents.getTransferData(getGUIClipboardPropertiesDataFlavor()); + ArrayList listOfProperties = gcp.getProperties(); + for (int i = 0; i < listOfProperties.size(); i++) + { + GUIProperty property = (GUIProperty) listOfProperties.get(i); + propList.addProperty(property.getPropString(), property.getComment()); + } + } + catch(UnsupportedFlavorException e) {} + catch(IOException e) {} } - catch(IOException e) - { + else + { + try + { + String text = (String)contents.getTransferData(java.awt.datatransfer.DataFlavor.stringFlavor); + propList.pastePropertiesString(text); + } + catch(UnsupportedFlavorException e) {} + catch(IOException e) {} } } } @@ -1174,6 +1191,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List else if(e instanceof GUIClipboardEvent) { GUIClipboardEvent ce = (GUIClipboardEvent)e; + if(ce.getComponent() == this || ce.getComponent() == propList) { if(!computing) @@ -2080,5 +2098,68 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List propList.notifySettings(settings); //the GUIPropertiesList object contains all of the "fast" data } + public static DataFlavor getGUIClipboardPropertiesDataFlavor() + { + return new DataFlavor(GUIClipboardProperties.class, "PRISM Property List"); + } + /** + * A class that allows sets of properties to be put on the clipboard. + */ + public class GUIClipboardProperties implements Transferable + { + private ArrayList listOfProperties; + private StringSelection stringRepresentation; + + public GUIClipboardProperties(ArrayList listOfProperties) + { + this.listOfProperties = listOfProperties; + String tmpString = ""; + for(int i = 0 ; i < listOfProperties.size(); i++) + { + GUIProperty gp = (GUIProperty)listOfProperties.get(i); + if (gp.getComment().trim().length() > 0) + { + tmpString += "//" + gp.getComment() + "\n"; + } + tmpString += gp.getPropString(); + if(i != listOfProperties.size() -1 ) tmpString += "\n"; + } + + stringRepresentation = new StringSelection(tmpString); + } + + + public Object getTransferData(DataFlavor flavor) throws UnsupportedFlavorException, IOException + { + if (flavor.getRepresentationClass() == this.getClass()) + { return this; } + else + { return this.stringRepresentation.getTransferData(flavor); } + } + + public DataFlavor[] getTransferDataFlavors() + { + DataFlavor[] stringFlavors = stringRepresentation.getTransferDataFlavors(); + + DataFlavor[] allFlavors = new DataFlavor[stringFlavors.length + 1]; + allFlavors[0] = GUIMultiProperties.getGUIClipboardPropertiesDataFlavor(); + + for (int i = 0; i < stringFlavors.length; i++) + { allFlavors[i+1] = stringFlavors[i]; } + + return allFlavors; + } + + public boolean isDataFlavorSupported(DataFlavor flavor) + { + return (stringRepresentation.isDataFlavorSupported(flavor) || flavor.equals(GUIMultiProperties.getGUIClipboardPropertiesDataFlavor())); + } + + public ArrayList getProperties() + { + return listOfProperties; + } + + } } diff --git a/prism/src/userinterface/properties/GUIPropertiesList.java b/prism/src/userinterface/properties/GUIPropertiesList.java index 122ce9cc..f897b293 100644 --- a/prism/src/userinterface/properties/GUIPropertiesList.java +++ b/prism/src/userinterface/properties/GUIPropertiesList.java @@ -70,6 +70,8 @@ public class GUIPropertiesList extends JList implements KeyListener addKeyListener(this); setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION); + + getInputMap().put(KeyStroke.getKeyStroke(KeyEvent.VK_C, InputEvent.CTRL_MASK), "none"); } //ACCESS METHODS @@ -227,7 +229,10 @@ public class GUIPropertiesList extends JList implements KeyListener while(sto.hasMoreTokens()) { String token = sto.nextToken(); - addProperty(token, ""); + + // Make sure it isn't comment we are pasting + if (token.indexOf("//") != 0) + addProperty(token, ""); } } @@ -377,49 +382,30 @@ public class GUIPropertiesList extends JList implements KeyListener { if(e.getModifiers() == KeyEvent.CTRL_MASK) { - if(e.getKeyCode() == KeyEvent.VK_V) + if(e.getKeyCode() == KeyEvent.VK_C) + { + parent.a_copy(); + } + else if(e.getKeyCode() == KeyEvent.VK_V) { - java.awt.datatransfer.Clipboard clipboard = Toolkit.getDefaultToolkit().getSystemClipboard(); - java.awt.datatransfer.Transferable contents = clipboard.getContents(null); - if(contents !=null) - { - try - { - String text = (String)contents.getTransferData(java.awt.datatransfer.DataFlavor.stringFlavor); - pastePropertiesString(text); - } - catch(java.awt.datatransfer.UnsupportedFlavorException ex) - { - } - catch(IOException ex) - { - } - } + parent.a_paste(); } else if(e.getKeyCode() == KeyEvent.VK_X) { - java.awt.datatransfer.Clipboard clipboard = Toolkit.getDefaultToolkit().getSystemClipboard(); - java.awt.datatransfer.StringSelection selection = new java.awt.datatransfer.StringSelection(getClipboardString()); - clipboard.setContents(selection, null); - - deleteSelected(); - parent.setModified(true); + parent.a_cut(); } else if(e.getKeyCode() == KeyEvent.VK_D) { - deleteSelected(); - parent.setModified(true); + parent.a_delete(); } else if(e.getKeyCode() == KeyEvent.VK_A) { - selectAll(); - } - + parent.a_selectAll(); + } } if(e.getKeyCode() == KeyEvent.VK_DELETE) { - deleteSelected(); - parent.setModified(true); + parent.a_delete(); } } diff --git a/prism/src/userinterface/properties/GUIProperty.java b/prism/src/userinterface/properties/GUIProperty.java index 00c6dcde..0fc76a58 100644 --- a/prism/src/userinterface/properties/GUIProperty.java +++ b/prism/src/userinterface/properties/GUIProperty.java @@ -1,6 +1,6 @@ //============================================================================== // -// Copyright (c) 2002-2004, Andrew Hinton, Dave Parker +// Copyright (c) 2002-2006, Andrew Hinton, Dave Parker, Mark Kattenbelt // // This file is part of PRISM. // @@ -27,6 +27,7 @@ import prism.*; import javax.swing.*; import java.lang.*; import java.net.*; +import java.awt.datatransfer.*; /** *