4,10 → 4,10 |
* Coded by: Group 5, software practice summer 2003 |
* University of Bielefeld, Germany |
* |
* @version $Revision: 1.76 $ |
* @version $Revision: 1.77 $ |
* |
* Last modification: $Date: 2003/07/21 14:56:02 $ |
* $Id: GUI.java,v 1.76 2003/07/21 14:56:02 hjokusch Exp $ |
* Last modification: $Date: 2003/07/22 06:31:31 $ |
* $Id: GUI.java,v 1.77 2003/07/22 06:31:31 swalkenh Exp $ |
*/ |
|
package src.gui; |
49,18 → 49,18 |
* <code> ActionListener</code> |
* @author group 5 |
* |
* @version $Revision: 1.76 $ Last modification: $Date: 2003/07/21 14:56:02 $ |
* @version $Revision: 1.77 $ Last modification: $Date: 2003/07/22 06:31:31 $ |
*/ |
public class GUI |
extends JFrame implements GuiInterface,WindowListener { |
|
|
//added 11/07/03 Sascha W.; testing with plugins - generate plugin-dependend menu |
/* Testing with plugins - generate plugin-dependend menu. */ |
private JMenuBar myMenuBar; |
private JMenu pluginMenu; |
private JMenu pluginConfigurationMenu; |
|
/* attributes for the menu */ |
/* Attributes for the menu. */ |
private JMenuItem exit; |
private JMenuItem open; |
|
73,37 → 73,38 |
private JMenuItem validate; |
private JMenuItem setNewDTD; |
private JMenuItem setNewSchema; |
|
|
/* Menu buttons for creating and closing documents. */ |
private JMenuItem neweeDoc; |
private JMenuItem closeActDoc; |
private JMenuItem closeAll; |
|
/* Menu buttons for the configuration of the plugins */ |
/* Menu buttons for the configuration of the plugins. */ |
private JMenuItem resetConfiguration; |
private JMenuItem changeDefaultPlugin; |
private JMenuItem switchToAndFroDefaultPlugin; |
private JMenuItem showActualConfiguration; |
|
/* attributes for logging and status */ |
/* Instance variables for the log and status panel. */ |
private LogPanel logPanel = new LogPanel(); |
private StatusPanel statusPanel = new StatusPanel(); |
|
/* attreibutes for changing view */ |
private JMenuItem setXpath; |
|
/* gui internal tree and its scroll pane*/ |
/* GUI internal tree and it's scroll pane. */ |
private PopUpJTree guiTree = new PopUpJTree(); |
private PopUpJTree tree = new PopUpJTree(); |
private JScrollPane treeScrollPane; |
|
/* attribut to put the elements in order */ |
private JSplitPane splitterMain; |
|
/* plugin panel -> uses double buffering. */ |
/* The plugin panel useing double buffering. */ |
private JPanel pluginPanel = new JPanel(true); |
|
/* A tabbed pane used to change between the different open documents. */ |
private JTabbedPane pluginTabbedPanel = new JTabbedPane(); |
|
/* attributes for linking events with objects*/ |
/* The required event listeners. */ |
private ActionListener otherGUIListener; |
private ActionListener validatorListener; |
private ActionListener docManager; |
110,6 → 111,8 |
private ActionListener updateViewListener; |
private ActionListener pluginManager; |
private ChangeListener docManagerCL; |
|
/* A reference variable to the document manager. */ |
private DocumentManagerInterface docMaster; |
|
|