diff --git a/prism/src/userinterface/GUIClipboard.java b/prism/src/userinterface/GUIClipboard.java index c939a2e3..db57bddc 100644 --- a/prism/src/userinterface/GUIClipboard.java +++ b/prism/src/userinterface/GUIClipboard.java @@ -27,27 +27,120 @@ package userinterface; import javax.swing.*; +import javax.swing.undo.UndoManager; + +import java.awt.Toolkit; +import java.awt.datatransfer.Clipboard; +import java.awt.datatransfer.FlavorEvent; +import java.awt.datatransfer.FlavorListener; import java.awt.event.*; + import userinterface.util.*; /** - * - * @author ug60axh + * This class gets notified through pluginChanged when the plugin in + * focus has changed. The undo/redo actions can be implemented cleanly + * by implementing the getUndoManager() function in GUIPlugin. Once this + * is done it should work automatically, including enabledness of these actions. + * + * The clipboard functions paste/copy/cut/select all/delete work slightly more + * complicated. This class listens on the focussed plugin's selectionChangeManager + * and calls canDoClipboardFunction on this plugin to determine enabledness. + * There is no need to pass changes in the clipboard state to the + * selectionChangeManager, as this is done automatically. Hence, only notify when + * a change in selection occurs. + * + * All actions can be and should be used as menu items. + * + * @author ug60axh, mxk */ public class GUIClipboard extends GUIPlugin { + /* the current GUIPlugin undoManager */ + private GUIPrism prism; + private GUIPlugin plugin; + private GUIUndoManager undoManager; private JMenu editMenu; private JToolBar editToolBar; - private Action menuActionCut, menuActionCopy, menuActionPaste, menuActionDelete, menuActionSelectAll; - private Action toolbarActionCut, toolbarActionCopy, toolbarActionPaste, toolbarActionDelete, toolbarActionSelectAll; - - + private Action actionUndo, actionRedo, actionCut, actionCopy, actionPaste, actionDelete, actionSelectAll; + /** Creates a new instance of GUIClipboard */ public GUIClipboard(GUIPrism pr) { super(pr, false); + this.prism = pr; initComponents(); + doUndoManagerEnables(); + doClipboardEnables(); + + /* Listen to clipboard events. */ + Clipboard clipboard = Toolkit.getDefaultToolkit().getSystemClipboard(); + clipboard.addFlavorListener(new FlavorListener() { + @Override + public void flavorsChanged(FlavorEvent e) { + doClipboardEnables(); + } + }); + } + + /* gets called when plugin changes. should implement this as an + * GUIEvent really */ + public void pluginChanged(GUIPlugin plugin) + { + if (plugin != null) + plugin.getSelectionChangeHandler().clear(); + + // remove listener + if (undoManager != null) + undoManager.clear(); + + this.plugin = null; + this.undoManager = null; + + if (plugin != null) + { + this.plugin = plugin; + /* get notified when enabledness of clipboard actions may change */ + this.plugin.getSelectionChangeHandler().addListener(new GUIEventListener() { + @Override + public boolean processGUIEvent(GUIEvent e) { + doClipboardEnables(); + return true; + } + }); + + if (plugin.getUndoManager() != null) + { + undoManager = plugin.getUndoManager(); + + /* get notified when undo history may change */ + undoManager.addListener(new GUIEventListener() { + @Override + public boolean processGUIEvent(GUIEvent e) { + if (e instanceof GUIUndoManagerEvent) + { + doUndoManagerEnables(); + return true; + } + + return false; + } + }); + } + } + + doUndoManagerEnables(); + doClipboardEnables(); } + private void doClipboardEnables() + { + actionCopy.setEnabled(plugin != null && plugin.canDoClipBoardAction(actionCopy)); + actionCut.setEnabled(plugin != null && plugin.canDoClipBoardAction(actionCut)); + actionPaste.setEnabled(plugin != null && plugin.canDoClipBoardAction(actionPaste)); + actionDelete.setEnabled(plugin != null && plugin.canDoClipBoardAction(actionDelete)); + actionSelectAll.setEnabled(plugin != null && plugin.canDoClipBoardAction(actionSelectAll)); + } + public void takeCLArgs(String args[]) { } @@ -91,188 +184,173 @@ public class GUIClipboard extends GUIPlugin return false; } + public void doUndoManagerEnables() + { + actionUndo.setEnabled(undoManager != null && undoManager.canUndo()); + actionRedo.setEnabled(undoManager != null && undoManager.canRedo()); + } + private void initComponents() { setupActions(); editMenu = new javax.swing.JMenu(); { - JMenuItem cut = new javax.swing.JMenuItem(); - cut.setAction(menuActionCut); - cut.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_X, InputEvent.CTRL_MASK)); - - JMenuItem copy = new javax.swing.JMenuItem(); - copy.setAction(menuActionCopy); - copy.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_C, InputEvent.CTRL_MASK)); - - JMenuItem paste = new javax.swing.JMenuItem(); - paste.setAction(menuActionPaste); - paste.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_V, InputEvent.CTRL_MASK)); - - JMenuItem delete = new javax.swing.JMenuItem(); - 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(menuActionSelectAll); - selectAll.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_A, InputEvent.CTRL_MASK)); - - editMenu.setMnemonic(KeyEvent.VK_E); + editMenu.setMnemonic(KeyEvent.VK_E); editMenu.setText("Edit"); - editMenu.add(cut); - editMenu.add(copy); - editMenu.add(paste); - editMenu.add(delete); - editMenu.add(jSeparator3); - editMenu.add(selectAll); + + editMenu.add(new JMenuItem(actionUndo)); + editMenu.add(new JMenuItem(actionRedo)); + editMenu.add(new JSeparator()); + editMenu.add(new JMenuItem(actionCut)); + editMenu.add(new JMenuItem(actionCopy)); + editMenu.add(new JMenuItem(actionPaste)); + editMenu.add(new JMenuItem(actionDelete)); + editMenu.add(new JSeparator()); + editMenu.add(new JMenuItem(actionSelectAll)); } editToolBar = new JToolBar(); { - JButton b1 = new JButton(toolbarActionCut); + + JButton b6 = new JButton(actionUndo); + b6.setToolTipText("Undo"); + b6.setText(""); + editToolBar.add(b6); + + JButton b7 = new JButton(actionRedo); + b7.setToolTipText("Redo"); + b7.setText(""); + editToolBar.add(b7); + + //editToolBar.add(new JSeparator()); + + JButton b1 = new JButton(actionCut); b1.setToolTipText("Cut"); b1.setText(""); editToolBar.add(b1); - JButton b2 = new JButton(toolbarActionCopy); + JButton b2 = new JButton(actionCopy); b2.setToolTipText("Copy"); b2.setText(""); editToolBar.add(b2); - JButton b3 = new JButton(toolbarActionPaste); + JButton b3 = new JButton(actionPaste); b3.setToolTipText("Paste"); b3.setText(""); editToolBar.add(b3); - JButton b4 = new JButton(toolbarActionDelete); + JButton b4 = new JButton(actionDelete); b4.setToolTipText("Delete"); b4.setText(""); editToolBar.add(b4); + + //editToolBar.add(new JSeparator()); + + JButton b5 = new JButton(actionSelectAll); + b5.setToolTipText("Select all"); + b5.setText(""); + editToolBar.add(b5); } editToolBar.setFloatable(false); } + /* Send GUIClipboardEvents to the focussed GUIPlugin */ + private void setupActions() { - menuActionCut = new AbstractAction() + actionUndo = new AbstractAction() { public void actionPerformed(ActionEvent e) { - notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.CUT, getFocussedComponent())); + notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.UNDO, getFocussedComponent())); } }; - menuActionCut.putValue(Action.LONG_DESCRIPTION, "Copys the currently selected item/text to the clipboard and then removes it."); - //actionCut.putValue(Action.SHORT_DESCRIPTION, "Cut"); - menuActionCut.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_C)); - menuActionCut.putValue(Action.NAME, "Cut"); - menuActionCut.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallCut.png")); + actionUndo.putValue(Action.LONG_DESCRIPTION, "Undo the last edit."); + actionUndo.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_U)); + actionUndo.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_Z, java.awt.event.InputEvent.CTRL_MASK)); + actionUndo.putValue(Action.NAME, "Undo"); + actionUndo.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallUndo.png")); - toolbarActionCut = new AbstractAction() + actionRedo = new AbstractAction() { public void actionPerformed(ActionEvent e) { - notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.CUT, getFocussedComponent())); + notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.REDO, 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.png")); - - - - menuActionCopy = new AbstractAction() + actionRedo.putValue(Action.LONG_DESCRIPTION, "Redo the last edit."); + actionRedo.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_R)); + actionRedo.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_Y, java.awt.event.InputEvent.CTRL_MASK)); + actionRedo.putValue(Action.NAME, "Redo"); + actionRedo.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallRedo.png")); + + + actionCut = new AbstractAction() { public void actionPerformed(ActionEvent e) { - notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.COPY, getFocussedComponent())); + notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.CUT, getFocussedComponent())); } }; - 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.png")); - - toolbarActionCopy = new AbstractAction() + actionCut.putValue(Action.LONG_DESCRIPTION, "Copys the currently selected item/text to the clipboard and then removes it."); + actionCut.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_C)); + actionCut.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_X, java.awt.event.InputEvent.CTRL_MASK)); + actionCut.putValue(Action.NAME, "Cut"); + actionCut.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallCut.png")); + + actionCopy = 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.png")); - - menuActionPaste = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.PASTE, getFocussedComponent())); - } - }; - 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.png")); - - toolbarActionPaste = new AbstractAction() + actionCopy.putValue(Action.LONG_DESCRIPTION, "Copys the currently selected item/text to the clipboard."); + actionCopy.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_O)); + actionCopy.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_C, java.awt.event.InputEvent.CTRL_MASK)); + actionCopy.putValue(Action.NAME, "Copy"); + actionCopy.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallCopy.png")); + + actionPaste = 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.png")); - - 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.png")); + actionPaste.putValue(Action.LONG_DESCRIPTION, "Pastes the contents of the clipboard."); + actionPaste.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_P)); + actionPaste.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_V, java.awt.event.InputEvent.CTRL_MASK)); + actionPaste.putValue(Action.NAME, "Paste"); + actionPaste.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallPaste.png")); + - toolbarActionDelete = new AbstractAction() + actionDelete = new AbstractAction() { public void actionPerformed(ActionEvent e) { notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.DELETE, getFocussedComponent())); } }; - toolbarActionDelete.putValue(Action.LONG_DESCRIPTION, "Removes the currently selected item"); - toolbarActionDelete.putValue(Action.NAME, "Delete"); - toolbarActionDelete.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallDelete.png")); - - 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.png")); + actionDelete.putValue(Action.LONG_DESCRIPTION, "Removes the currently selected item"); + actionDelete.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_D)); + actionDelete.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_D, java.awt.event.InputEvent.CTRL_MASK)); + actionDelete.putValue(Action.NAME, "Delete"); + actionDelete.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallDelete.png")); - toolbarActionSelectAll = new AbstractAction() + actionSelectAll = new AbstractAction() { public void actionPerformed(ActionEvent e) { notifyEventListeners(new GUIClipboardEvent(GUIClipboardEvent.SELECT_ALL, getFocussedComponent())); } }; - 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.png")); + actionSelectAll.putValue(Action.LONG_DESCRIPTION, "Selects all items of the focussed component."); + actionSelectAll.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_S)); + actionSelectAll.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_A, java.awt.event.InputEvent.CTRL_MASK)); + actionSelectAll.putValue(Action.NAME, "Select all"); + actionSelectAll.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallSelectAll.png")); } public OptionsPanel getOptions() @@ -282,5 +360,40 @@ public class GUIClipboard extends GUIPlugin public void notifySettings(prism.PrismSettings settings) {} + + public Action getUndoAction() { + return actionUndo; + } + + public Action getRedoAction() { + return actionRedo; + } + + public Action getCutAction() { + return actionCut; + } + + public Action getCopyAction() { + return actionCopy; + } + + public Action getPasteAction() { + return actionPaste; + } + + public Action getDeleteAction() { + return actionDelete; + } + + public Action getSelectAllAction() { + return actionSelectAll; + } + + + + + + + } diff --git a/prism/src/userinterface/GUIClipboardEvent.java b/prism/src/userinterface/GUIClipboardEvent.java index 98429ff5..f68db51d 100644 --- a/prism/src/userinterface/GUIClipboardEvent.java +++ b/prism/src/userinterface/GUIClipboardEvent.java @@ -26,7 +26,6 @@ //============================================================================== package userinterface; -import javax.swing.undo.UndoManager; import java.awt.*; @@ -38,14 +37,13 @@ import userinterface.util.*; */ public class GUIClipboardEvent extends GUIEvent { - private UndoManager undoManager; - - public static final int COPY = 0; + public static final int COPY = 0; public static final int CUT = 1; public static final int PASTE = 2; public static final int DELETE = 3; public static final int SELECT_ALL = 4; - public static final int UNDOMANAGER_CHANGE = 5; + public static final int UNDO = 5; + public static final int REDO = 6; static int counter =0; /** Creates a new instance of GUIClipboardEvent */ @@ -60,15 +58,4 @@ public class GUIClipboardEvent extends GUIEvent { return (GUIPlugin)getData(); } - - public UndoManager getUndoManager() - { - return undoManager; - } - - public void setUndoManager(UndoManager undoManager) - { - this.undoManager = undoManager; - } - } diff --git a/prism/src/userinterface/GUIPlugin.java b/prism/src/userinterface/GUIPlugin.java index effc6215..601c7f5d 100644 --- a/prism/src/userinterface/GUIPlugin.java +++ b/prism/src/userinterface/GUIPlugin.java @@ -72,6 +72,12 @@ public abstract class GUIPlugin extends JPanel implements GUIEventListener, Pris private GUIPrism gui; private Prism prism; + /** Whenever the state of the cut/copy/delete/selectall buttons should change + * notify this handler. This will in turn call the canDoClipBoardAction to + * determine which buttons should be enabled. + */ + protected GUIEventHandler selectionChangeHandler; + //CONSTRUCTORS /** This is the super constructor that all implementing subclasses should call, it @@ -85,10 +91,19 @@ public abstract class GUIPlugin extends JPanel implements GUIEventListener, Pris { this.gui = gui; this.prism = gui.getPrism(); + selectionChangeHandler = new GUIEventHandler(gui); if(listens)gui.getEventHandler().addListener(this); setPreferredSize(new Dimension(800,600)); } + + public GUIEventHandler getSelectionChangeHandler() + { + return selectionChangeHandler; + } + + + /** This is the super constructor that all implementing subclasses should call, it * sets up the interaction with the top level GUI, and also sets up the * interaction with the event @@ -164,6 +179,22 @@ public abstract class GUIPlugin extends JPanel implements GUIEventListener, Pris return gui; } + /** Returns the top level user interface + * @return the GUI. + */ + public GUIUndoManager getUndoManager() + { + return null; + } + + /** Determine whether or not this action should be enabled. + * @param: action An action in GUIClipboard (but not undo/redo). + */ + public boolean canDoClipBoardAction(Action action) + { + return false; + } + /** Utility access method to access which component is focussed in the top level * GUI. * @return The focussed component in the GUI. diff --git a/prism/src/userinterface/GUIPrism.java b/prism/src/userinterface/GUIPrism.java index 62718cda..4d5c5d32 100644 --- a/prism/src/userinterface/GUIPrism.java +++ b/prism/src/userinterface/GUIPrism.java @@ -33,6 +33,8 @@ import java.net.*; import java.awt.*; import java.awt.event.*; import javax.swing.*; +import javax.swing.event.ChangeEvent; +import javax.swing.event.ChangeListener; import javax.swing.plaf.*; import javax.swing.plaf.metal.*; //Prism Packages @@ -69,7 +71,7 @@ public class GUIPrism extends JFrame private static GUIPrismSplash splash; private static GUIPrism gui; private boolean doExit; - + private static GUIClipboard clipboardPlugin; //STATIC METHODS @@ -112,7 +114,8 @@ public class GUIPrism extends JFrame ArrayList plugs = new ArrayList(); //Define Plugins here plugs.add(new userinterface.GUIFileMenu(g)); // File menu - plugs.add(new userinterface.GUIClipboard(g)); // Clipboard + clipboardPlugin = new GUIClipboard(g); + plugs.add(clipboardPlugin); // Clipboard plugs.add(new userinterface.model.GUIMultiModel(g)); userinterface.simulator.GUISimulator sim = new userinterface.simulator.GUISimulator(g); plugs.add(new userinterface.properties.GUIMultiProperties(g, sim)); @@ -227,7 +230,12 @@ public class GUIPrism extends JFrame //options.addPanel(new GUIPrismOptionsPanel(prism)); JPanel thePanel = new JPanel(); // panel to store tabs theTabs = new JTabbedPane(); - + theTabs.addChangeListener(new ChangeListener() { + @Override + public void stateChanged(ChangeEvent e) { + clipboardPlugin.pluginChanged(getFocussedPlugin()); + } + }); //Setup pluggable screens in here plugs = getPluginArray(this); for(int i = 0; i < plugs.size(); i++) @@ -540,13 +548,14 @@ public class GUIPrism extends JFrame if(c instanceof GUIPlugin) { GUIPlugin pl = (GUIPlugin)c; + if(pl == tab) { - theTabs.setEnabledAt(i, enable); - break; + theTabs.setEnabledAt(i, enable); + break; } } - } + } } /** Moves the view to the next GUIPlugin component which has a tab. If the last one @@ -633,4 +642,8 @@ public class GUIPrism extends JFrame splash.dispose(); } } + + public static GUIClipboard getClipboardPlugin() { + return clipboardPlugin; + } } diff --git a/prism/src/userinterface/log/GUILog.java b/prism/src/userinterface/log/GUILog.java index 18134c1b..18b0ac27 100644 --- a/prism/src/userinterface/log/GUILog.java +++ b/prism/src/userinterface/log/GUILog.java @@ -30,6 +30,7 @@ import java.io.*; import java.awt.*; import java.awt.event.*; import javax.swing.*; + import userinterface.*; import prism.PrismLog; import userinterface.util.*; @@ -44,9 +45,11 @@ public class GUILog extends GUIPlugin implements MouseListener, PrismSettingsLis private PrismLog theLog; private JTextArea text; private JPopupMenu popupMenu; + private JMenu logMenu; + //private GUILogOptions options; private GUIPrismFileFilter textFilter[]; - + private Action clearAction, saveAction; private int maxTextLengthFast; /** Creates a new instance of GUILog */ @@ -81,7 +84,7 @@ public class GUILog extends GUIPlugin implements MouseListener, PrismSettingsLis public javax.swing.JMenu getMenu() { - return null; + return logMenu; } public String getTabText() @@ -122,9 +125,37 @@ public class GUILog extends GUIPlugin implements MouseListener, PrismSettingsLis theLog.print(le.getData()); } } + else if (e instanceof GUIClipboardEvent) + { + GUIClipboardEvent ce = (GUIClipboardEvent)e; + if(ce.getID() == GUIClipboardEvent.COPY) + { + ((GUIWindowLog)theLog).copy(); + return true; + } + else if(ce.getID() == GUIClipboardEvent.SELECT_ALL) + { + ((GUIWindowLog)theLog).selectAll(); + return true; + } + } return false; } + @Override + public boolean canDoClipBoardAction(Action action) + { + if (action == GUIPrism.getClipboardPlugin().getCopyAction()) + { + return ((GUIWindowLog)theLog).hasSelectedText(); + } + else if (action == GUIPrism.getClipboardPlugin().getSelectAllAction()) + { + return true; + } + return false; + } + private void initComponentsAsWindowLog(GUIWindowLog log) { JScrollPane logScroller = new JScrollPane(); @@ -133,7 +164,7 @@ public class GUILog extends GUIPlugin implements MouseListener, PrismSettingsLis text.addMouseListener(this); text.setFont(new Font("monospaced", Font.PLAIN, 12)); text.setBackground(Color.lightGray); - log.open(text); + log.open(text, this); text.addMouseListener(this); text.setEditable(false); text.setBorder(new javax.swing.border.TitledBorder("Log Output")); @@ -145,8 +176,10 @@ public class GUILog extends GUIPlugin implements MouseListener, PrismSettingsLis add(logScroller, BorderLayout.CENTER); popupMenu = new JPopupMenu(); + logMenu = new JMenu("Log"); - Action clearAction = new AbstractAction() + + clearAction = new AbstractAction() { public void actionPerformed(ActionEvent e) { @@ -156,8 +189,9 @@ public class GUILog extends GUIPlugin implements MouseListener, PrismSettingsLis clearAction.putValue(Action.SHORT_DESCRIPTION, "Clear log"); clearAction.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_C)); clearAction.putValue(Action.NAME, "Clear log"); + clearAction.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallDelete.png")); - Action saveAction = new AbstractAction() + saveAction = new AbstractAction() { public void actionPerformed(ActionEvent e) { @@ -180,12 +214,25 @@ public class GUILog extends GUIPlugin implements MouseListener, PrismSettingsLis } } }; - saveAction.putValue(Action.SHORT_DESCRIPTION, "Save log"); + saveAction.putValue(Action.SHORT_DESCRIPTION, "Save log as..."); saveAction.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_S)); - saveAction.putValue(Action.NAME, "Save log"); + saveAction.putValue(Action.NAME, "Save log as..."); + saveAction.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallSave.png")); - popupMenu.add(clearAction); + + //popupMenu.add(new JSeparator()); popupMenu.add(saveAction); + popupMenu.add(new JSeparator()); + popupMenu.add(GUIPrism.getClipboardPlugin().getCopyAction()); + popupMenu.add(clearAction); + popupMenu.add(new JSeparator()); + popupMenu.add(GUIPrism.getClipboardPlugin().getSelectAllAction()); + + + logMenu.setMnemonic('L'); + logMenu.add(saveAction); + logMenu.add(new JSeparator()); + logMenu.add(clearAction); textFilter = new GUIPrismFileFilter[1]; textFilter[0] = new GUIPrismFileFilter("Plain text files (*.txt)"); diff --git a/prism/src/userinterface/log/GUIWindowLog.java b/prism/src/userinterface/log/GUIWindowLog.java index f87ad6cf..810b8742 100644 --- a/prism/src/userinterface/log/GUIWindowLog.java +++ b/prism/src/userinterface/log/GUIWindowLog.java @@ -28,9 +28,13 @@ package userinterface.log; import javax.swing.*; +import javax.swing.event.CaretEvent; +import javax.swing.event.CaretListener; import javax.swing.text.BadLocationException; import prism.*; +import userinterface.GUIPlugin; +import userinterface.util.GUIEvent; public class GUIWindowLog implements PrismLog { @@ -42,25 +46,35 @@ public class GUIWindowLog implements PrismLog private String buffer; // clear flag private boolean clearFlag; + private GUILog logPlugin; public GUIWindowLog() { + buffer = ""; clearFlag = false; textArea = null; updater = null; } - public GUIWindowLog(JTextArea ta) + public GUIWindowLog(JTextArea ta, GUILog logPlugin) { buffer = ""; clearFlag = false; - open(ta); + open(ta, logPlugin); } - public void open(JTextArea ta) + public void open(JTextArea ta, GUILog logPlugin) { + this.logPlugin = logPlugin; textArea = ta; + textArea.addCaretListener(new CaretListener() { + @Override + public void caretUpdate(CaretEvent e) { + if (GUIWindowLog.this.logPlugin != null) + GUIWindowLog.this.logPlugin.getSelectionChangeHandler().notifyListeners(new GUIEvent(1)); + } + }); updater = new GUIWindowLogUpdater(this, textArea); updater.start(); } @@ -323,6 +337,23 @@ public class GUIWindowLog implements PrismLog textArea.setBackground(settings.getColor(PrismSettings.LOG_BG_COLOUR)); setMaxTextLength(settings.getInteger(PrismSettings.LOG_BUFFER_LENGTH)); } + + public boolean hasSelectedText() + { + return (textArea != null && textArea.getSelectedText() != null); + } + + public void copy() + { + if (textArea != null) + textArea.copy(); + } + + public void selectAll() + { + if (textArea != null) + textArea.selectAll(); + } } //------------------------------------------------------------------------------ diff --git a/prism/src/userinterface/model/GUIModelEditor.java b/prism/src/userinterface/model/GUIModelEditor.java index 4f6a10b9..00eb5a7d 100644 --- a/prism/src/userinterface/model/GUIModelEditor.java +++ b/prism/src/userinterface/model/GUIModelEditor.java @@ -29,17 +29,21 @@ package userinterface.model; import javax.swing.*; import prism.PrismLangException; +import userinterface.util.GUIUndoManager; /** * * @author ug60axh */ public abstract class GUIModelEditor extends JPanel -{ - +{ public abstract String getParseText(); public abstract void newModel(); + public abstract void undo(); + + public abstract void redo(); + public abstract void cut(); public abstract void copy(); @@ -53,4 +57,14 @@ public abstract class GUIModelEditor extends JPanel public void modelParseFailed(PrismLangException parserError, boolean background) {} public void modelParseSuccessful() {} + + public GUIUndoManager getUndoManager() + { + return null; + } + + public boolean canDoClipBoardAction(Action action) + { + return false; + } } diff --git a/prism/src/userinterface/model/GUIMultiModel.java b/prism/src/userinterface/model/GUIMultiModel.java index 7c707c85..3584a2db 100644 --- a/prism/src/userinterface/model/GUIMultiModel.java +++ b/prism/src/userinterface/model/GUIMultiModel.java @@ -27,7 +27,9 @@ package userinterface.model; import userinterface.*; + import javax.swing.*; + import java.awt.*; import java.awt.event.*; import java.io.*; @@ -638,7 +640,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener computeTr.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_T)); computeTr.putValue(Action.NAME, "Transient probabilities"); computeTr.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallClockAnim1.png")); - computeTr.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_F5, 0)); + computeTr.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_F4, KeyEvent.CTRL_DOWN_MASK)); viewStates = new AbstractAction() { public void actionPerformed(ActionEvent e) { a_viewBuild(GUIMultiModelHandler.STATES_EXPORT, Prism.EXPORT_PLAIN); } }; @@ -749,6 +751,11 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener handler.delete(); else if(id == GUIClipboardEvent.SELECT_ALL) handler.selectAll(); + else if(id == GUIClipboardEvent.UNDO) + handler.undo(); + else if(id == GUIClipboardEvent.REDO) + handler.redo(); + } } else if(e instanceof GUIComputationEvent) @@ -757,17 +764,19 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener { computing = true; doEnables(); + selectionChangeHandler.notifyListeners(new GUIEvent(1)); } else if(e.getID() == GUIComputationEvent.COMPUTATION_DONE) { computing = false; doEnables(); + selectionChangeHandler.notifyListeners(new GUIEvent(1)); } else if(e.getID() == GUIComputationEvent.COMPUTATION_ERROR) { - computing = false; doEnables(); + selectionChangeHandler.notifyListeners(new GUIEvent(1)); } } else if (e instanceof GUIExitEvent) @@ -783,50 +792,9 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener return false; } - private void initComponents() + private JMenu initExportMenu() { - setupActions(); - - JPanel topPanel = new JPanel(); - { - fileLabel = new JLabel(); - { - fileLabel.setHorizontalAlignment(javax.swing.SwingConstants.LEFT); - fileLabel.setBorder(new javax.swing.border.EtchedBorder()); - fileLabel.setMinimumSize(new java.awt.Dimension(40, 25)); - } - - //progress = new JProgressBar(0, 100); - topPanel.setLayout(new BorderLayout()); - handler = new GUIMultiModelHandler(this); - //topPanel.add(progress, BorderLayout.WEST); - topPanel.add(fileLabel,BorderLayout.NORTH); - topPanel.add(handler,BorderLayout.CENTER); - } - - setLayout(new BorderLayout()); - add(topPanel, BorderLayout.CENTER); - - modelMenu = new JMenu("Model"); - newMenu = new JMenu("New"); - newMenu.setMnemonic('N'); - newMenu.setIcon(GUIPrism.getIconFromImage("smallNew.png")); - newMenu.add(newPRISMModel); - if (GM_ENABLED) newMenu.add(newGraphicModel); - newMenu.add(newPEPAModel); - modelMenu.add(newMenu); - modelMenu.add(new JSeparator()); - modelMenu.add(loadModel); - modelMenu.add(reloadModel); - modelMenu.add(new JSeparator()); - modelMenu.add(saveModel); - modelMenu.add(saveAsModel); - modelMenu.add(new JSeparator()); - modelMenu.setMnemonic(KeyEvent.VK_M); - modelMenu.add(parseModel); - modelMenu.add(buildModel); - modelMenu.add(new JSeparator()); - exportMenu = new JMenu("Export"); + JMenu exportMenu = new JMenu("Export"); exportMenu.setMnemonic('E'); exportMenu.setIcon(GUIPrism.getIconFromImage("smallExport.png")); exportStatesMenu = new JMenu("States"); @@ -857,8 +825,12 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener exportTransRewardsMenu.add(exportTransRewardsMatlab); exportTransRewardsMenu.add(exportTransRewardsMRMC); exportMenu.add(exportTransRewardsMenu); - modelMenu.add(exportMenu); - viewMenu = new JMenu("View"); + return exportMenu; + } + + private JMenu initViewMenu() + { + JMenu viewMenu = new JMenu("View"); viewMenu.setMnemonic('V'); viewMenu.setIcon(GUIPrism.getIconFromImage("smallView.png")); viewMenu.add(viewStates); @@ -866,12 +838,68 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener viewMenu.add(viewStateRewards); viewMenu.add(viewTransRewards); viewMenu.add(viewPrismCode); - modelMenu.add(viewMenu); - computeMenu = new JMenu("Compute"); + return viewMenu; + } + + private JMenu initComputeMenu() + { + JMenu computeMenu = new JMenu("Compute"); computeMenu.setMnemonic('C'); computeMenu.setIcon(GUIPrism.getIconFromImage("smallCompute.png")); computeMenu.add(computeSS); computeMenu.add(computeTr); + return computeMenu; + } + + private void initComponents() + { + setupActions(); + + modelMenu = new JMenu("Model"); + exportMenu = initExportMenu(); + viewMenu = initViewMenu(); + computeMenu = initComputeMenu(); + + JPanel topPanel = new JPanel(); + { + fileLabel = new JLabel(); + { + fileLabel.setHorizontalAlignment(javax.swing.SwingConstants.LEFT); + fileLabel.setBorder(new javax.swing.border.EtchedBorder()); + fileLabel.setMinimumSize(new java.awt.Dimension(40, 25)); + } + + //progress = new JProgressBar(0, 100); + topPanel.setLayout(new BorderLayout()); + handler = new GUIMultiModelHandler(this); + //topPanel.add(progress, BorderLayout.WEST); + topPanel.add(fileLabel,BorderLayout.NORTH); + topPanel.add(handler,BorderLayout.CENTER); + } + + newMenu = new JMenu("New"); + newMenu.setMnemonic('N'); + newMenu.setIcon(GUIPrism.getIconFromImage("smallNew.png")); + newMenu.add(newPRISMModel); + if (GM_ENABLED) newMenu.add(newGraphicModel); + newMenu.add(newPEPAModel); + modelMenu.add(newMenu); + modelMenu.add(new JSeparator()); + modelMenu.add(loadModel); + modelMenu.add(reloadModel); + modelMenu.add(new JSeparator()); + modelMenu.add(saveModel); + modelMenu.add(saveAsModel); + modelMenu.add(new JSeparator()); + modelMenu.setMnemonic(KeyEvent.VK_M); + modelMenu.add(parseModel); + modelMenu.add(buildModel); + modelMenu.add(new JSeparator()); + + modelMenu.add(exportMenu); + + modelMenu.add(viewMenu); + modelMenu.add(computeMenu); popup = new JPopupMenu(); @@ -904,6 +932,11 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener dotFilter[0] = new GUIPrismFileFilter("Dot files (*.dot)"); dotFilter[0].addExtension("dot"); + + + setLayout(new BorderLayout()); + add(topPanel, BorderLayout.CENTER); + doEnables(); } @@ -918,5 +951,40 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener handler.notifySettings(settings); repaint(); - } + } + + @Override + public GUIUndoManager getUndoManager() + { + return handler.getUndoManager(); + } + + @Override + public boolean canDoClipBoardAction(Action action) { + // TODO Auto-generated method stub + if (computing) + return false; + + return handler.canDoClipBoardAction(action); + } + + public AbstractAction getParseModel() { + return parseModel; + } + + public AbstractAction getBuildModel() { + return buildModel; + } + + public JMenu getViewMenu() { + return initViewMenu(); + } + + public JMenu getExportMenu() { + return initExportMenu(); + } + + public JMenu getComputeMenu() { + return initComputeMenu(); + } } diff --git a/prism/src/userinterface/model/GUIMultiModelHandler.java b/prism/src/userinterface/model/GUIMultiModelHandler.java index c54c5f24..5d256fbc 100644 --- a/prism/src/userinterface/model/GUIMultiModelHandler.java +++ b/prism/src/userinterface/model/GUIMultiModelHandler.java @@ -1075,7 +1075,6 @@ public class GUIMultiModelHandler extends JPanel public void hasModified(boolean attemptReparse) { - modified = true; if(isBusy()) { @@ -1110,6 +1109,16 @@ public class GUIMultiModelHandler extends JPanel theModel.doEnables(); } + public void undo() + { + editor.undo(); + } + + public void redo() + { + editor.redo(); + } + public void cut() { editor.cut(); @@ -1522,4 +1531,21 @@ public class GUIMultiModelHandler extends JPanel } } } + + public GUIUndoManager getUndoManager() + { + return editor.getUndoManager(); + } + + public boolean canDoClipBoardAction(Action action) { + // TODO Auto-generated method stub + return editor.canDoClipBoardAction(action); + } + + public void jumpToError() { + if (editor != null && editor instanceof GUITextModelEditor) + ((GUITextModelEditor)editor).jumpToError(); + } + + } diff --git a/prism/src/userinterface/model/GUITextModelEditor.java b/prism/src/userinterface/model/GUITextModelEditor.java index e6850810..da1cf699 100644 --- a/prism/src/userinterface/model/GUITextModelEditor.java +++ b/prism/src/userinterface/model/GUITextModelEditor.java @@ -37,20 +37,27 @@ import javax.swing.undo.CannotUndoException; import javax.swing.undo.UndoManager; import java.awt.*; import java.awt.event.ActionEvent; +import java.awt.event.InputEvent; import java.awt.event.KeyEvent; import java.awt.event.MouseEvent; import java.awt.event.MouseListener; import java.awt.datatransfer.Clipboard; import javax.swing.event.*; + import java.io.*; +import java.util.ArrayList; import java.util.HashMap; +import java.util.Iterator; import java.util.Map; import prism.PrismLangException; import prism.PrismSettings; import prism.PrismSettingsListener; import userinterface.GUIClipboardEvent; +import userinterface.GUIPlugin; import userinterface.GUIPrism; +import userinterface.util.GUIEvent; +import userinterface.util.GUIUndoManager; /** Editing pane with syntax highlighting and line numbers etc for text * model files. Currently supports Prism and Pepa models. It also tells @@ -58,7 +65,6 @@ import userinterface.GUIPrism; */ public class GUITextModelEditor extends GUIModelEditor implements DocumentListener, MouseListener { - private GUIMultiModelHandler handler; /** Standard java editor component for editing the model files. A custom * editor kit is used to provide syntax highlighting and line numbers. @@ -68,7 +74,7 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen /** Allows undo/redo operations to be performed on the model editor. */ - private UndoManager undoManager; + private GUIUndoManager undoManager; private JScrollPane editorScrollPane; /** The line numbers etc. gutter for the model editor. */ private GUITextModelEditorGutter gutter; @@ -82,7 +88,7 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen private JPopupMenu contextPopup; /** Actions for the context menu. */ - private Action actionCut, actionCopy, actionPaste, actionUndo, actionRedo, actionSearch, actionJumpToError; + private Action actionSearch, actionJumpToError; /** More actions */ private Action insertDTMC, insertCTMC, insertMDP; @@ -168,12 +174,17 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen editor.setEditable(true); editor.setText(initialText); editor.getDocument().addDocumentListener(this); - editor.getDocument().addUndoableEditListener(new EditorUndoableEditListener()); + editor.addCaretListener(new CaretListener() { + @Override + public void caretUpdate(CaretEvent e) { + GUITextModelEditor.this.handler.getGUIPlugin().getSelectionChangeHandler().notifyListeners(new GUIEvent(1)); + } + }); editor.getDocument().putProperty( PlainDocument.tabSizeAttribute, new Integer(4) ); editor.addMouseListener(this); errorHighlightPainter = new DefaultHighlighter.DefaultHighlightPainter(new Color(255,192,192)); - undoManager = new UndoManager(); + undoManager = new GUIUndoManager(GUIPrism.getGUI()); undoManager.setLimit(200); // Setup the scrollpane @@ -211,52 +222,49 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen // method to initialize the context menu popup initContextMenu(); - - InputMap inputMap = editor.getInputMap(); - inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_Z, java.awt.event.InputEvent.CTRL_MASK), "undo"); - inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_Y, java.awt.event.InputEvent.CTRL_MASK), "redo"); - inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_Z, java.awt.event.InputEvent.CTRL_MASK | java.awt.event.InputEvent.SHIFT_MASK), "redo"); + + InputMap inputMap = editor.getInputMap(); + inputMap.clear(); + + inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_Z, java.awt.event.InputEvent.CTRL_MASK), "prism_undo"); + inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_Z, java.awt.event.InputEvent.CTRL_MASK), "prism_undo"); + inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_Y, java.awt.event.InputEvent.CTRL_MASK), "prism_redo"); + inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_A, java.awt.event.InputEvent.CTRL_MASK), "prism_selectall"); + inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_D, java.awt.event.InputEvent.CTRL_MASK), "prism_delete"); + inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_X, java.awt.event.InputEvent.CTRL_MASK), "prism_cut"); + inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_V, java.awt.event.InputEvent.CTRL_MASK), "prism_paste"); + inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_E, java.awt.event.InputEvent.CTRL_MASK), "prism_jumperr"); + inputMap.put(KeyStroke.getKeyStroke(KeyEvent.VK_Z, java.awt.event.InputEvent.CTRL_MASK | java.awt.event.InputEvent.SHIFT_MASK), "prism_redo"); ActionMap actionMap = editor.getActionMap(); - actionMap.put("undo", actionUndo); - actionMap.put("redo", actionRedo); + actionMap.put("prism_undo", GUIPrism.getClipboardPlugin().getUndoAction()); + actionMap.put("prism_redo", GUIPrism.getClipboardPlugin().getRedoAction()); + actionMap.put("prism_selectall", GUIPrism.getClipboardPlugin().getSelectAllAction()); + actionMap.put("prism_cut", GUIPrism.getClipboardPlugin().getCutAction()); + actionMap.put("prism_copy", GUIPrism.getClipboardPlugin().getCopyAction()); + actionMap.put("prism_paste", GUIPrism.getClipboardPlugin().getPasteAction()); + actionMap.put("prism_delete", GUIPrism.getClipboardPlugin().getDeleteAction()); + actionMap.put("prism_jumperr", actionJumpToError); + + editor.getDocument().addUndoableEditListener(undoManager); + editor.getDocument().addUndoableEditListener(new UndoableEditListener() + { + @Override + public void undoableEditHappened(UndoableEditEvent e) + { + System.out.println("adding undo edit"); + } + }); } /** * Helper method to initialize the actions used for the buttons. */ private void initActions() { - actionCut = new AbstractAction() { - public void actionPerformed(ActionEvent ae) { - editor.cut(); - } - }; - 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() { - public void actionPerformed(ActionEvent ae) { - editor.copy(); - } - }; - actionCopy.putValue(Action.LONG_DESCRIPTION, "Copies the highlighted text to the clipboard."); - actionCopy.putValue(Action.NAME, "Copy"); - //actionCopy.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("editcopy.png")); - - actionPaste = new AbstractAction() { - public void actionPerformed(ActionEvent ae) { - editor.paste(); - } - }; - actionPaste.putValue(Action.LONG_DESCRIPTION, "Pastes the text stored in the clipboard."); - actionPaste.putValue(Action.NAME, "Paste"); - //actionPaste.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("editpaste.png")); - - actionUndo = new AbstractAction() { + /*actionUndo = new AbstractAction() { public void actionPerformed(ActionEvent ae) { try { // do redo @@ -295,7 +303,7 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen actionRedo.putValue(Action.LONG_DESCRIPTION, "Redos the most recent undo"); actionRedo.putValue(Action.NAME, "Redo"); actionRedo.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallRedo.png")); - + */ actionJumpToError = new AbstractAction() { public void actionPerformed(ActionEvent ae) { jumpToError(); @@ -304,6 +312,7 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen actionJumpToError.putValue(Action.NAME, "Jump to error"); actionJumpToError.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("tinyError.png")); + actionJumpToError.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_E, InputEvent.CTRL_MASK)); // search and replace action @@ -393,15 +402,25 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen * */ private void initContextMenu() { + contextPopup = new JPopupMenu(); - contextPopup.add(actionUndo); - contextPopup.add(actionRedo); + contextPopup.add(GUIPrism.getClipboardPlugin().getUndoAction()); + contextPopup.add(GUIPrism.getClipboardPlugin().getRedoAction()); + contextPopup.add(new JSeparator()); + contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getParseModel()); + contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getBuildModel()); contextPopup.add(new JSeparator()); - contextPopup.add(actionCut); - contextPopup.add(actionCopy); - contextPopup.add(actionPaste); + contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getExportMenu()); + contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getViewMenu()); + contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getComputeMenu()); contextPopup.add(new JSeparator()); - contextPopup.add(actionJumpToError); + contextPopup.add(GUIPrism.getClipboardPlugin().getCutAction()); + contextPopup.add(GUIPrism.getClipboardPlugin().getCopyAction()); + contextPopup.add(GUIPrism.getClipboardPlugin().getPasteAction()); + contextPopup.add(GUIPrism.getClipboardPlugin().getDeleteAction()); + contextPopup.add(new JSeparator()); + contextPopup.add(GUIPrism.getClipboardPlugin().getSelectAllAction()); + //contextPopup.add(actionJumpToError); //contextPopup.add(actionSearch); @@ -445,13 +464,15 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen */ public void read(Reader reader, Object object) throws IOException { + editor.getDocument().removeUndoableEditListener(undoManager); + editor.read(reader, object); // For some unknown reason the listeners have to be added both here // and in the constructor, if they're not added here the editor won't // be listening. - editor.getDocument().addDocumentListener(this); - editor.getDocument().addUndoableEditListener(new EditorUndoableEditListener()); + editor.getDocument().addDocumentListener(this); + editor.getDocument().addUndoableEditListener(undoManager); } public void setText(String text) @@ -502,7 +523,8 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen */ public void insertUpdate(DocumentEvent event) { - if (handler != null) handler.hasModified(true); + if (handler != null) + handler.hasModified(true); } @@ -512,7 +534,8 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen */ public void removeUpdate(DocumentEvent event) { - if (handler != null) handler.hasModified(true); + if (handler != null) + handler.hasModified(true); } public String getParseText() @@ -526,6 +549,7 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen try { undoManager.undo(); } catch (CannotUndoException ex) { + //GUIPrism.getGUI().getMultiLogger().logMessage(PrismLogLevel.PRISM_ERROR, ex.getMessage()); } } @@ -591,26 +615,7 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen { editor.setBackground(c); } - - /** Listens for changes made to the model editor and updates the UndoManager, - * allowing undo/redo operations to be performed. - */ - protected class EditorUndoableEditListener implements UndoableEditListener - { - public void undoableEditHappened(UndoableEditEvent e) - { - // Remember the edit and raise a listener event for any - // other interested objects. - undoManager.addEdit(e.getEdit()); - GUIClipboardEvent clipboardEvent = new GUIClipboardEvent(GUIClipboardEvent.UNDOMANAGER_CHANGE, - handler.getGUIPlugin().getFocussedComponent()); - // Send the undo manager with the event so that interested - // objects can determine the state of the undo manager. - clipboardEvent.setUndoManager(undoManager); - GUIPrism.getGUI().notifyEventListeners(clipboardEvent); - } - } - + // rajk public JEditorPane getEditorPane(){ return this.editor; @@ -628,7 +633,7 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen public void mousePressed(MouseEvent me) { if (me.isPopupTrigger()) { - + /* // check if to have paste enabled or not Clipboard clipboard = Toolkit.getDefaultToolkit().getSystemClipboard(); @@ -648,24 +653,14 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen actionCut.setEnabled(true); actionCopy.setEnabled(true); } - + */ // check undo - if (undoManager.canUndo()) { - actionUndo.setEnabled(true); - } - else { - actionUndo.setEnabled(false); - } - - // check redo - if (undoManager.canRedo()) { - actionRedo.setEnabled(true); - } - else { - actionRedo.setEnabled(false); - } + //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()); @@ -757,7 +752,7 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen while (parserChar < column) { - if (text.charAt(documentChar) == '\t') + if (documentChar < text.length() && text.charAt(documentChar) == '\t') { parserChar += 8; documentChar += 1; @@ -786,7 +781,31 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen this.parseError = null; // get rid of any error highlighting refreshErrorDisplay(); - } - + } + + public GUIUndoManager getUndoManager() + { + return undoManager; + } + public boolean canDoClipBoardAction(Action action) { + if (action == GUIPrism.getClipboardPlugin().getPasteAction()) + { + Clipboard clipboard = Toolkit.getDefaultToolkit().getSystemClipboard(); + return (clipboard.getContents(null) != null); + } + else if ( + action == GUIPrism.getClipboardPlugin().getCutAction() || + action == GUIPrism.getClipboardPlugin().getCopyAction() || + action == GUIPrism.getClipboardPlugin().getDeleteAction()) + { + return (editor.getSelectedText() != null); + } + else if (action == GUIPrism.getClipboardPlugin().getSelectAllAction()) + { + return true; + } + + return handler.canDoClipBoardAction(action); + } } diff --git a/prism/src/userinterface/model/graphicModel/GUIGraphicModelEditor.java b/prism/src/userinterface/model/graphicModel/GUIGraphicModelEditor.java index c3463c1f..3469d71e 100644 --- a/prism/src/userinterface/model/graphicModel/GUIGraphicModelEditor.java +++ b/prism/src/userinterface/model/graphicModel/GUIGraphicModelEditor.java @@ -103,6 +103,16 @@ public class GUIGraphicModelEditor extends GUIModelEditor implements SelectionLi return "GUIGRAPHICMODELEDITOR IS ME"; } + public void undo() + { + + } + + public void redo() + { + + } + public void copy() { diff --git a/prism/src/userinterface/model/pepaModel/GUIPepaModelEditor.java b/prism/src/userinterface/model/pepaModel/GUIPepaModelEditor.java index ac0ca90b..fbd752dd 100644 --- a/prism/src/userinterface/model/pepaModel/GUIPepaModelEditor.java +++ b/prism/src/userinterface/model/pepaModel/GUIPepaModelEditor.java @@ -29,6 +29,10 @@ package userinterface.model.pepaModel; import javax.swing.*; import javax.swing.text.*; +import javax.swing.undo.CannotRedoException; +import javax.swing.undo.CannotUndoException; +import javax.swing.undo.UndoManager; + import java.util.regex.*; import java.awt.*; import javax.swing.event.*; @@ -40,9 +44,9 @@ import userinterface.model.*; * @author ug60axh */ public class GUIPepaModelEditor extends GUIModelEditor implements DocumentListener -{ - +{ private JEditorPane editor; + private UndoManager undoManager; private PlainDocument d; private GUIMultiModelHandler handler; @@ -53,6 +57,8 @@ public class GUIPepaModelEditor extends GUIModelEditor implements DocumentListen PepaEditorKit kit = new PepaEditorKit(); editor.setEditorKitForContentType("text/pepa", kit); editor.setContentType("text/pepa"); + undoManager = new UndoManager(); + undoManager.setLimit(200); //editor.setForeground(FOREGROUND_COLOR); this.handler = handler; d = (PlainDocument)editor.getDocument(); @@ -108,6 +114,27 @@ public class GUIPepaModelEditor extends GUIModelEditor implements DocumentListen editor.write(s); } + /** Performs an undo operation on the text in the model editor. + */ + public void undo() { + try { + undoManager.undo(); + } catch (CannotUndoException ex) { + + //GUIPrism.getGUI().getMultiLogger().logMessage(PrismLogLevel.PRISM_ERROR, ex.getMessage()); + } + } + + /** Performs a redo operation on the text in the model editor. + */ + public void redo() { + try { + undoManager.redo(); + } catch (CannotRedoException ex) { + //GUIPrism.getGUI().getMultiLogger().logMessage(PrismLogLevel.PRISM_ERROR, ex.getMessage()); + } + } + public void copy() { editor.copy(); diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 8d82204a..5334777f 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -33,6 +33,7 @@ import java.util.*; import java.awt.*; import java.awt.event.*; import java.awt.datatransfer.*; + import javax.swing.*; import javax.swing.event.*; import javax.swing.border.*; @@ -50,7 +51,7 @@ import parser.ast.*; /** * Properties tab of the PRISM GUI. */ -public class GUIMultiProperties extends GUIPlugin implements MouseListener, ListSelectionListener, PrismSettingsListener +public class GUIMultiProperties extends GUIPlugin implements MouseListener, ListSelectionListener, PrismSettingsListener, ContainerListener { //CONSTANTS public static final int CONTINUE = 0; @@ -92,8 +93,8 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List private Vector clipboardVector; private Action newProps, openProps, saveProps, savePropsAs, insertProps, - verifySelected, cutAction, copyAction, pasteAction, deleteAction, - newProperty, editProperty, selectAllAction, newConstant, + verifySelected, + newProperty, editProperty, newConstant, removeConstant, newLabel, removeLabel, newExperiment, deleteExperiment, stopExperiment, viewResults, plotResults, exportResults, simulate, details; @@ -476,6 +477,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List // Force repaint because we modified the GUIProperty directly repaintList(); } + selectionChangeHandler.notifyListeners(new GUIEvent(1)); updateCommentLabel(); } @@ -522,6 +524,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List { computing = com; doEnables(); + selectionChangeHandler.notifyListeners(new GUIEvent(1)); } protected void setActiveFile(File f) @@ -567,11 +570,6 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List propList.setEnabled (!computing); newProperty.setEnabled (!computing); editProperty.setEnabled (!computing && propList.getSelectedProperties().size() > 0); - cutAction.setEnabled (!computing); - copyAction.setEnabled (!computing); - pasteAction.setEnabled (!computing); - deleteAction.setEnabled (!computing); - selectAllAction.setEnabled (!computing); // constants list removeConstant.setEnabled(consTable.getSelectedRowCount() > 0); // label list @@ -935,6 +933,8 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List ed.show(); } } + + selectionChangeHandler.notifyListeners(new GUIEvent(1)); } public void a_selectAll() @@ -1264,9 +1264,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List if(!computing) { if(e.isPopupTrigger() && e.getSource() == propList) - { - - + { int index = propList.locationToIndex(e.getPoint()); // if there are no properties selected, select the one under the popup if(propList.isSelectionEmpty()) @@ -1294,6 +1292,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List propList.setSelectedIndex(index); } } + // disable certain actions if any of the selected propeties are currently being edited int[] sel = propList.getSelectedIndices(); boolean showDeleters = true; @@ -1304,12 +1303,8 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List showDeleters = false; break; } - } - + } - - cutAction.setEnabled(true); - deleteAction.setEnabled(true); verifySelected.setEnabled(propList.getValidSelectedProperties().size() > 0); simulate.setEnabled(propList.getValidSimulatableSelectedProperties().size() > 0); details.setEnabled(propList.getValidSelectedProperties().size() > 0); @@ -1319,8 +1314,6 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List if(showDeleters == false) { - cutAction.setEnabled(false); - deleteAction.setEnabled(false); simulate.setEnabled(false); verifySelected.setEnabled(false); details.setEnabled(false); @@ -1343,11 +1336,50 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List doEnables(); this.experimentPopup.show(e.getComponent(), e.getX(), e.getY()); } - } + } + } + + @Override + public boolean canDoClipBoardAction(Action action) + { + if (computing) + return false; + + // disable certain actions if any of the selected propeties are currently being edited + int[] sel = propList.getSelectedIndices(); + boolean showDeleters = true; + for(int i = 0; i < sel.length; i++) + { + if(propList.getProperty(sel[i]).isBeingEdited()) + { + showDeleters = false; + break; + } + } + if (action == GUIPrism.getClipboardPlugin().getPasteAction()) + { + Clipboard clipboard = Toolkit.getDefaultToolkit().getSystemClipboard(); + return (clipboard.getContents(null) != null); + } + else if (action == GUIPrism.getClipboardPlugin().getCutAction() || + action == GUIPrism.getClipboardPlugin().getDeleteAction()) + { + if (!showDeleters) return false; + return (propList.getSelectedProperties().size() > 0); + } + else if (action == GUIPrism.getClipboardPlugin().getCopyAction()) + { + return (propList.getSelectedProperties().size() > 0); + } + else if (action == GUIPrism.getClipboardPlugin().getSelectAllAction()) + { + return true; + } + return false; } - + public void mouseReleased(MouseEvent e) { removeConstant.setEnabled(consTable.getSelectedRowCount() > 0); @@ -1394,8 +1426,6 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List break; } } - cutAction.setEnabled(true); - deleteAction.setEnabled(true); verifySelected.setEnabled(propList.getValidSelectedProperties().size() > 0); simulate.setEnabled(propList.getValidSimulatableSelectedProperties().size() > 0); details.setEnabled(propList.getValidSelectedProperties().size() > 0); @@ -1404,8 +1434,6 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List if(showDeleters == false) { - cutAction.setEnabled(false); - deleteAction.setEnabled(false); simulate.setEnabled(false); verifySelected.setEnabled(false); details.setEnabled(false); @@ -1432,6 +1460,21 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List } } + + + @Override + public void componentAdded(ContainerEvent e) + { + // notify GUIClipboard + selectionChangeHandler.notifyListeners(new GUIEvent(1)); + } + + @Override + public void componentRemoved(ContainerEvent e) { + // notify GUIClipboard + selectionChangeHandler.notifyListeners(new GUIEvent(1)); + } + //METHODS TO IMPLEMENT ListSelectionListener INTERFACE public void valueChanged(ListSelectionEvent e) { @@ -1447,16 +1490,14 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List break; } } - cutAction.setEnabled(true); - deleteAction.setEnabled(true); + verifySelected.setEnabled(propList.getValidSelectedProperties().size() > 0); simulate.setEnabled(propList.getValidSimulatableSelectedProperties().size() > 0); details.setEnabled(propList.getValidSelectedProperties().size() > 0); editProperty.setEnabled(propList.getSelectedProperties().size() > 0); + if(showDeleters == false) { - cutAction.setEnabled(false); - deleteAction.setEnabled(false); simulate.setEnabled(false); verifySelected.setEnabled(false); details.setEnabled(false); @@ -1469,6 +1510,9 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List removeConstant.setEnabled(consTable.getSelectedRowCount() > 0); removeLabel.setEnabled(labTable.getSelectedRowCount() > 0); + + // notify GUIClipboard + selectionChangeHandler.notifyListeners(new GUIEvent(1)); } //CONSTRUCTOR HELPER METHODS @@ -1491,6 +1535,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List { propList = new GUIPropertiesList(getPrism(), this); propList.addListSelectionListener(this); + propList.addContainerListener(this); propScroll.setViewportView(propList); } JScrollPane comScroll = new JScrollPane(); @@ -1657,12 +1702,12 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List propertiesPopup.add(newExperiment); propertiesPopup.add(details); propertiesPopup.add(new JSeparator()); - propertiesPopup.add(cutAction); - propertiesPopup.add(copyAction); - propertiesPopup.add(pasteAction); - propertiesPopup.add(deleteAction); + propertiesPopup.add(GUIPrism.getClipboardPlugin().getCutAction()); + propertiesPopup.add(GUIPrism.getClipboardPlugin().getCopyAction()); + propertiesPopup.add(GUIPrism.getClipboardPlugin().getPasteAction()); + propertiesPopup.add(GUIPrism.getClipboardPlugin().getDeleteAction()); propertiesPopup.add(new JSeparator()); - propertiesPopup.add(selectAllAction); + propertiesPopup.add(GUIPrism.getClipboardPlugin().getSelectAllAction()); constantsPopup = new JPopupMenu(); @@ -1797,56 +1842,6 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List verifySelected.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallTick.png")); verifySelected.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_F5, 0)); - cutAction = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - a_cut(); - } - }; - cutAction.putValue(Action.LONG_DESCRIPTION, "Copys the selected properties to the clipboard and then deletes them."); - //cutAction.putValue(Action.SHORT_DESCRIPTION, "Cut"); - cutAction.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_T)); - cutAction.putValue(Action.NAME, "Cut"); - cutAction.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallCut.png")); - //cutAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_X, InputEvent.CTRL_MASK)); - - copyAction = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - a_copy(); - } - }; - copyAction.putValue(Action.LONG_DESCRIPTION, "Copys the selected properties to the clipboard."); - copyAction.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_C)); - copyAction.putValue(Action.NAME, "Copy"); - copyAction.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallCopy.png")); - - pasteAction = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - a_paste(); - } - }; - pasteAction.putValue(Action.LONG_DESCRIPTION, "Pastes the properties on the clipboard to the properties list"); - pasteAction.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_P)); - pasteAction.putValue(Action.NAME, "Paste"); - pasteAction.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallPaste.png")); - - deleteAction = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - a_delete(); - } - }; - deleteAction.putValue(Action.LONG_DESCRIPTION, "Deletes the selected properties."); - deleteAction.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_D)); - deleteAction.putValue(Action.NAME, "Delete"); - deleteAction.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallDelete.png")); - newProperty = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -1870,19 +1865,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List editProperty.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_E)); editProperty.putValue(Action.NAME, "Edit"); editProperty.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallEdit.png")); - - selectAllAction = new AbstractAction() - { - public void actionPerformed(ActionEvent e) - { - a_selectAll(); - } - }; - selectAllAction.putValue(Action.LONG_DESCRIPTION, "Selects all properties in the properties list"); - selectAllAction.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_A)); - selectAllAction.putValue(Action.NAME, "Select all"); - selectAllAction.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallSelectAll.png")); - + newConstant = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -2076,8 +2059,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List } stringRepresentation = new StringSelection(tmpString); - } - + } public Object getTransferData(DataFlavor flavor) throws UnsupportedFlavorException, IOException { @@ -2108,7 +2090,6 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List public ArrayList getProperties() { return listOfProperties; - } - + } } } diff --git a/prism/src/userinterface/util/GUIEventHandler.java b/prism/src/userinterface/util/GUIEventHandler.java index dd03b0c6..1a04f069 100644 --- a/prism/src/userinterface/util/GUIEventHandler.java +++ b/prism/src/userinterface/util/GUIEventHandler.java @@ -60,7 +60,16 @@ public class GUIEventHandler if (res) break; } // notify gui itself - if (!res) gui.processGUIEvent(e); + if (gui != null && !res) gui.processGUIEvent(e); } + public boolean removeListener(GUIEventListener listen) + { + return listeners.remove(listen); + } + + public void clear() + { + listeners.clear(); + } }