4,10 → 4,10 |
* Coded by: Group 5, software practice summer 2003 |
* University of Bielefeld, Germany |
* |
* @version $Revision: 1.88 $ |
* @version $Revision: 1.87 $ |
* |
* Last modification: $Date: 2003/07/28 11:42:20 $ |
* $Id: GUI.java,v 1.88 2003/07/28 11:42:20 swalkenh Exp $ |
* Last modification: $Date: 2003/07/26 15:55:59 $ |
* $Id: GUI.java,v 1.87 2003/07/26 15:55:59 smcsporr Exp $ |
*/ |
|
package src.gui; |
51,12 → 51,13 |
* |
* @author group 5 |
* |
* @version $Revision: 1.88 $ Last modification: $Date: 2003/07/28 11:42:20 $ |
* @version $Revision: 1.87 $ Last modification: $Date: 2003/07/26 15:55:59 $ |
*/ |
public class GUI |
extends JFrame implements GuiInterface, WindowListener { |
extends JFrame implements GuiInterface,WindowListener { |
|
/** Generate plugin-dependend menu. */ |
|
/* Testing with plugins - generate plugin-dependend menu. */ |
private JMenuBar myMenuBar; |
private JMenu pluginMenu; |
private JMenu pluginConfigurationMenu; |
71,8 → 72,8 |
private JMenuItem saveAll; |
|
/** Menu buttons for validation and grammar setting functions. */ |
private JMenuItem validate; |
private JCheckBoxMenuItem autoValidate; |
private JMenuItem validate; |
private JMenuItem setNewDTD; |
private JMenuItem setNewSchema; |
private JMenuItem removeDTD; |
97,7 → 98,7 |
private JMenuItem setXpath; |
private JMenuItem clearLogPanel; |
|
/** Tree display and it's scroll pane. */ |
/* GUI internal tree and it's scroll pane. */ |
private PopUpJTree guiTree = new PopUpJTree(); |
private PopUpJTree tree = new PopUpJTree(); |
private JScrollPane treeScrollPane; |
104,10 → 105,10 |
|
private JSplitPane splitterMain; |
|
/** A panel to show plugin content and functions in. */ |
/* The plugin panel useing double buffering. */ |
private JPanel pluginPanel = new JPanel(true); |
|
/** A tabbed pane used to change between the different open documents. */ |
/* A tabbed pane used to change between the different open documents. */ |
private JTabbedPane pluginTabbedPanel = new JTabbedPane(); |
|
/** The required event listeners. */ |
127,8 → 128,8 |
* and produces a frame to draw on. |
*/ |
public GUI() { |
// make menu |
|
// make menu |
getContentPane().setLayout(new BorderLayout()); |
|
/* set up toolbar panel with double buffering. |
779,7 → 780,7 |
/** |
* Sets the panel object the plugins will use to draw their content. |
* |
* @param newPanel The <code>JPanel</code> that will be used for displaying. |
* @param newPanel: The <code>JPanel</code> that will be used for displaying. |
* |
* author S. Walkenhorst |
*/ |
796,7 → 797,7 |
* specified, an empty and disabled menu item will be displayed. The menu will change |
* each time, when another plugin than the current one sends it's menu object. |
* |
* @param newPluginMenu The <code>JMenu</code> object with appropriate content. |
* @param newPluginMenu: The <code>JMenu</code> object with appropriate content. |
* |
* author S. Walkenhorst |
* |
845,7 → 846,7 |
* the program's tabbed pane will be closed and the program will quit and exit |
* to the OS. |
* |
* @param event The 'close' window event. |
* @param event: The 'close' window event. |
* |
* @see java.awt.event.WindowEvent |
* @see java.awt.event.WindowListener |