| java.lang.Object
 de.uka.ilkd.key.gui.RecentFileMenu
| RecentFileMenu | | public class RecentFileMenu (Code) | | This class offers a mechanism to manage recent files; it adds the
necessary menu items to a menu or even can provide that menu itself.
also it offers a way to read the recent files from a java.util.Properties
object and can store them again to a Properties object.
This class is a result of the fusion of the RecentFileBuffer and RecentFiles
classes.
It's not a Menu in itself!!!
author:
Ute Platzer, with a lot of input from Volker Braun. |
| Inner Class :public static class RecentFileEntry | |
| Constructor Summary | |
| public | RecentFileMenu(ActionListener listener, int maxNumberOfEntries, Properties p)
Create a new RecentFiles list.
Parameters:
listener - the ActionListener that will be notified of the userclicked on a recent file menu entry. |
| RecentFileMenu | | public RecentFileMenu(ActionListener listener, int maxNumberOfEntries, Properties p)(Code) | | Create a new RecentFiles list.
Parameters:
listener - the ActionListener that will be notified of the userclicked on a recent file menu entry. The selected filename can bedetermined with the ActionEvent's getSource() method, cast the Objectinto a JMenuItem and call the getLabel() method.
Parameters:
maxNumberOfEntries - the maximal number of items/entries in therecent file menu.
Parameters:
p - a Properties object containing information about the recentfiles to be displayed initially.Or null to use no initial information. |
| addRecentFile | | public void addRecentFile(String name)(Code) | | call this method to add a new file to the beginning of the RecentFiles
list. If the name is already part of the list, it will be moved to the
first position. No more than a specified maximum number of names will
be allowed in the list, and additional names will be removed at the end.
(set the maximum number with the
RecentFileMenu.setMaxNumberOfEntries(int i) method).
Parameters:
name - the name of the file. |
| getMenu | | public JMenu getMenu()(Code) | | the menu where the recent files are kept. If the user didn't specify
one in the constructor, a new JMenu is created. It can be accessed
via this method.
|
| getMostRecent | | public RecentFileEntry getMostRecent()(Code) | | |
| load | | public void load(Properties p)(Code) | | read the recent file names from the properties object.
the property names are expected to be "RecentFile0" "RecentFile1" ...
|
| load | | public void load(String filename)(Code) | | read the recent files from the given properties file
|
| setMaxNumberOfEntries | | public void setMaxNumberOfEntries(int max)(Code) | | specify the maximal number of recent files in the list.
The default is 5
|
| store | | public void store(Properties p)(Code) | | Put the names of the recent Files into the properties object.
The property names are "RecentFile0" "RecentFile1" ...
The values are fully qualified path names.
|
| store | | public void store(String filename)(Code) | | write the recent file names to the given properties file.
the file will be read (if it exists) and then re-written so no
information will be lost.
|
|
|