| 4,10 → 4,10 |
|---|
| * Coded by: Group 5, software practice summer 2003 |
| * University of Bielefeld, Germany |
| * |
| * @version $Revision: 1.8 $ |
| * @version $Revision: 1.9 $ |
| * |
| * Last modification: $Date: 2003/07/24 22:18:06 $ |
| * $Id: PluginManagerInterface.java,v 1.8 2003/07/24 22:18:06 ioklasse Exp $ |
| * Last modification: $Date: 2003/07/25 18:18:27 $ |
| * $Id: PluginManagerInterface.java,v 1.9 2003/07/25 18:18:27 swalkenh Exp $ |
| */ |
| |
| package src.plugins; |
| 26,7 → 26,7 |
|---|
| * |
| * @author Sascha Walkenhorst |
| * |
| * @version $Revision: 1.8 $ Last modification: $Date: 2003/07/24 22:18:06 $ |
| * @version $Revision: 1.9 $ Last modification: $Date: 2003/07/25 18:18:27 $ |
| */ |
| public interface PluginManagerInterface { |
| |
| 55,6 → 55,16 |
|---|
| |
| |
| /** |
| * Saves the name of the default plugin in the configuration. |
| * |
| * author Sascha Walkenhorst |
| * |
| * Last revision: 26-Jul-2003 by Sascha W. |
| */ |
| public void saveConfiguration(); |
| |
| |
| /** |
| * Delivers the name of the associated plugin to given element. |
| * If no plugin is explicitly associated with the given element |
| * the default plugin is returned. |