| 4,10 → 4,10 |
|---|
| * Coded by: Group 5, software practice summer 2003 |
| * University of Bielefeld, Germany |
| * |
| * @version $Revision: 1.84 $ |
| * @version $Revision: 1.85 $ |
| * |
| * Last modification: $Date: 2003/07/25 13:50:56 $ |
| * $Id: GUI.java,v 1.84 2003/07/25 13:50:56 hjokusch Exp $ |
| * Last modification: $Date: 2003/07/26 10:49:54 $ |
| * $Id: GUI.java,v 1.85 2003/07/26 10:49:54 smcsporr Exp $ |
| */ |
| |
| package src.gui; |
| 28,6 → 28,7 |
|---|
| import java.io.File; |
| |
| import javax.swing.AbstractAction; |
| import javax.swing.JCheckBoxMenuItem; |
| import javax.swing.JFrame; |
| import javax.swing.JMenu; |
| import javax.swing.JMenuBar; |
| 50,7 → 51,7 |
|---|
| * |
| * @author group 5 |
| * |
| * @version $Revision: 1.84 $ Last modification: $Date: 2003/07/25 13:50:56 $ |
| * @version $Revision: 1.85 $ Last modification: $Date: 2003/07/26 10:49:54 $ |
| */ |
| public class GUI |
| extends JFrame implements GuiInterface,WindowListener { |
| 72,6 → 73,7 |
|---|
| |
| /** Menu buttons for validation and grammar setting functions. */ |
| private JMenuItem validate; |
| private JCheckBoxMenuItem autoValidate; |
| private JMenuItem setNewDTD; |
| private JMenuItem setNewSchema; |
| private JMenuItem removeDTD; |
| 320,6 → 322,11 |
|---|
| validate.addActionListener(docManager); |
| documentMenu.add(validate); |
| |
| autoValidate = new JCheckBoxMenuItem("Auto validation", true); |
| /* Help text for auto validation feature. */ |
| autoValidate.setToolTipText("select to enable auto validation"); |
| documentMenu.add(autoValidate); |
| |
| documentMenu.addSeparator(); |
| |
| /* Menu item for changing a document's DTD. */ |