| 4,10 → 4,10 |
|---|
| * Coded by: Group 5, software practice summer 2003 |
| * University of Bielefeld, Germany |
| * |
| * @version $Revision: 1.80 $ |
| * @version $Revision: 1.81 $ |
| * |
| * Last modification: $Date: 2003/07/24 13:55:51 $ |
| * $Id: GUI.java,v 1.80 2003/07/24 13:55:51 smcsporr Exp $ |
| * Last modification: $Date: 2003/07/24 19:01:43 $ |
| * $Id: GUI.java,v 1.81 2003/07/24 19:01:43 smcsporr Exp $ |
| */ |
| |
| package src.gui; |
| 50,7 → 50,7 |
|---|
| * |
| * @author group 5 |
| * |
| * @version $Revision: 1.80 $ Last modification: $Date: 2003/07/24 13:55:51 $ |
| * @version $Revision: 1.81 $ Last modification: $Date: 2003/07/24 19:01:43 $ |
| */ |
| public class GUI |
| extends JFrame implements GuiInterface,WindowListener { |
| 698,6 → 698,16 |
|---|
| return docMaster.getActualDocumentFile(); |
| } |
| |
| /** |
| * Returns the document manager. |
| * |
| * @return The document manager. |
| */ |
| public DocumentManagerInterface getDocumentManagerInterface() |
| { |
| return docMaster; |
| } |
| |
| /** |
| * Returns the current plugin panel. |
| * |