4,10 → 4,10 |
* Coded by: Group 5, software practice summer 2003 |
* University of Bielefeld, Germany |
* |
* @version $Revision: 1.49 $ |
* @version $Revision: 1.50 $ |
* |
* Last modification: $Date: 2003/07/22 06:31:31 $ |
* $Id: PluginManager.java,v 1.49 2003/07/22 06:31:31 swalkenh Exp $ |
* Last modification: $Date: 2003/07/22 14:06:58 $ |
* $Id: PluginManager.java,v 1.50 2003/07/22 14:06:58 swalkenh Exp $ |
*/ |
|
package src.plugins; |
55,7 → 55,7 |
* |
* @author Sascha Walkenhorst |
* |
* @version $Revision: 1.49 $ Last modification: $Date: 2003/07/22 06:31:31 $ |
* @version $Revision: 1.50 $ Last modification: $Date: 2003/07/22 14:06:58 $ |
*/ |
public class PluginManager implements TreeSelectionListener, |
PluginManagerInterface, |
1142,33 → 1142,6 |
|
|
/** |
* This method is called if the active document changes. |
* |
* @param newActivDocumentName The name of the new active document. |
* |
* TODO what while changing document ? |
* |
* author Sascha Walkenhorst |
* |
* Last Revision: 16-Jul-2003 by Sascha W. |
*/ |
public void documentChanged(String newActivDocumentName) { |
// LinkedList lL = (LinkedList) documents.get(newActivDocumentName); |
// /* case: entry for "newActivDocumentName" exists */ |
// if (lL != null) { |
// /* get 'PluginLoader' of active plugin for the new active document */ |
// String activePlugin = (String) lL.getFirst(); |
// PluginLoader pL = (PluginLoader) ((Hashtable) plugins.get(activePlugin)).get("loader"); |
// |
// /* commit the internal "ownOurEventListener" to PluginLoader and force him to |
// * commit the listener to the plugin */ |
// pL.setOurEventListener(ownOurEventListener); |
// pL.commitOurEventListener(newActivDocumentName); |
// } |
} |
|
|
/** |
* ... |
* |
* TODO set up, comment |