s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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
master
Mark Kattenbelt 20 years ago
parent
03bd972419
commit
683a4c53e7
4 changed files with 211 additions and 94 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 141
      prism/src/userinterface/GUIClipboard.java
  2. 113
      prism/src/userinterface/properties/GUIMultiProperties.java
  3. 48
      prism/src/userinterface/properties/GUIPropertiesList.java
  4. 3
      prism/src/userinterface/properties/GUIProperty.java

141
prism/src/userinterface/GUIClipboard.java
View File

@ -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()

113
prism/src/userinterface/properties/GUIMultiProperties.java
View File

@ -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;
}
}
}

48
prism/src/userinterface/properties/GUIPropertiesList.java
View File

@ -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();
}
}

3
prism/src/userinterface/properties/GUIProperty.java
View File

@ -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.*;
/**
*

Write Preview
Loading…
Cancel
Save