| 4,10 → 4,10 |
|---|
| * Coded by: Group 5, software practice summer 2003 |
| * University of Bielefeld, Germany |
| * |
| * @version $Revision: 1.134 $ |
| * @version $Revision: 1.135 $ |
| * |
| * Last modification: $Date: 2003/07/28 13:21:09 $ |
| * $Id: DocumentManager.java,v 1.134 2003/07/28 13:21:09 smcsporr Exp $ |
| * Last modification: $Date: 2003/07/28 13:25:30 $ |
| * $Id: DocumentManager.java,v 1.135 2003/07/28 13:25:30 smcsporr Exp $ |
| */ |
| |
| package src.control; |
| 50,7 → 50,7 |
|---|
| * |
| * @author Group 5 |
| * |
| * @version $Revision: 1.134 $ Last modification: $Date: 2003/07/28 13:21:09 $ |
| * @version $Revision: 1.135 $ Last modification: $Date: 2003/07/28 13:25:30 $ |
| */ |
| public class DocumentManager implements ActionListener, DocumentManagerInterface, |
| ChangeListener { |
| 580,7 → 580,7 |
|---|
| if (! openDocumentList.isEmpty()) { |
| |
| /* Simple search algorithm to find the document. */ |
| for (int i=0;i<(openDocumentList.size()-1);++i) { |
| for (int i=0;i<(openDocumentList.size());i++) { |
| StringBuffer worker = new StringBuffer(); |
| // Compare the searched title with every found title. |
| worker.append(((OurDocument)(openDocumentList.get(i))).getTitle()); |
| 809,7 → 809,10 |
|---|
| |
| /* Check if the current index is > -1 for a valide selection */ |
| if (z > -1) { |
| try{ |
| changeToDocument(pluginTabbedPane.getTitleAt(pluginTabbedPane.getSelectedIndex())); |
| }catch(Exception e){ |
| } |
| |
| } |
| updateView.update(); |