4,10 → 4,10 |
* Coded by: Group 5, software practice summer 2003 |
* University of Bielefeld, Germany |
* |
* @version $Revision: 1.77 $ |
* @version $Revision: 1.78 $ |
* |
* Last modification: $Date: 2003/07/22 06:31:31 $ |
* $Id: GUI.java,v 1.77 2003/07/22 06:31:31 swalkenh Exp $ |
* Last modification: $Date: 2003/07/23 12:05:35 $ |
* $Id: GUI.java,v 1.78 2003/07/23 12:05:35 smcsporr Exp $ |
*/ |
|
package src.gui; |
49,7 → 49,7 |
* <code> ActionListener</code> |
* @author group 5 |
* |
* @version $Revision: 1.77 $ Last modification: $Date: 2003/07/22 06:31:31 $ |
* @version $Revision: 1.78 $ Last modification: $Date: 2003/07/23 12:05:35 $ |
*/ |
public class GUI |
extends JFrame implements GuiInterface,WindowListener { |
366,25 → 366,25 |
* Last Revision: 21-Jul-2003 by Sascha W. |
*/ |
private JMenu createPluginConfigurationMenu() { |
pluginConfigurationMenu = new JMenu("plugin configuration"); |
pluginConfigurationMenu = new JMenu("Plugin configuration"); |
|
resetConfiguration = new JMenuItem("reset configuration"); |
resetConfiguration = new JMenuItem("Reset Configuration"); |
resetConfiguration.setToolTipText("click to reset the plugin configuration"); |
resetConfiguration.addActionListener(pluginManager); |
pluginConfigurationMenu.add(resetConfiguration); |
|
changeDefaultPlugin = new JMenuItem("change default plugin"); |
changeDefaultPlugin = new JMenuItem("Change default plugin"); |
changeDefaultPlugin.setToolTipText("click to choose a other plugin as the default plugin"); |
changeDefaultPlugin.addActionListener(pluginManager); |
pluginConfigurationMenu.add(changeDefaultPlugin); |
|
switchToAndFroDefaultPlugin = new JMenuItem("switch to and fro default plugin"); |
switchToAndFroDefaultPlugin = new JMenuItem("Switch to and fro default plugin"); |
switchToAndFroDefaultPlugin.setToolTipText("click to switch between the associated and the default plugin"); |
switchToAndFroDefaultPlugin.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_D, Event.CTRL_MASK));; |
switchToAndFroDefaultPlugin.addActionListener(pluginManager); |
pluginConfigurationMenu.add(switchToAndFroDefaultPlugin); |
|
showActualConfiguration = new JMenuItem("show actual configuration"); |
showActualConfiguration = new JMenuItem("Show actual configuration"); |
showActualConfiguration.setToolTipText("click to show the actual plugin configuration"); |
showActualConfiguration.addActionListener(pluginManager); |
pluginConfigurationMenu.add(showActualConfiguration); |