Browse Source

improved handling of undo/redo/clipboard events

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@820 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Mark Kattenbelt 18 years ago
parent
commit
ecc854535a
  1. 341
      prism/src/userinterface/GUIClipboard.java
  2. 19
      prism/src/userinterface/GUIClipboardEvent.java
  3. 31
      prism/src/userinterface/GUIPlugin.java
  4. 25
      prism/src/userinterface/GUIPrism.java
  5. 63
      prism/src/userinterface/log/GUILog.java
  6. 37
      prism/src/userinterface/log/GUIWindowLog.java
  7. 18
      prism/src/userinterface/model/GUIModelEditor.java
  8. 168
      prism/src/userinterface/model/GUIMultiModel.java
  9. 28
      prism/src/userinterface/model/GUIMultiModelHandler.java
  10. 199
      prism/src/userinterface/model/GUITextModelEditor.java
  11. 10
      prism/src/userinterface/model/graphicModel/GUIGraphicModelEditor.java
  12. 31
      prism/src/userinterface/model/pepaModel/GUIPepaModelEditor.java
  13. 181
      prism/src/userinterface/properties/GUIMultiProperties.java
  14. 11
      prism/src/userinterface/util/GUIEventHandler.java

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

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

31
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.

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

63
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)");

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

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

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

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

199
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);
}
}

10
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()
{

31
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();

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

11
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();
}
}
Loading…
Cancel
Save