public class RecentFileMenu
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
RecentFileMenu.RecentFileEntry |
Constructor and Description |
---|
RecentFileMenu(KeYMediator mediator)
Create a new RecentFiles list.
|
Modifier and Type | Method and Description |
---|---|
void |
addRecentFile(java.lang.String name)
call this method to add a new file to the beginning of the RecentFiles
list.
|
java.lang.String |
getAbsolutePath(javax.swing.JMenuItem item) |
javax.swing.JMenu |
getMenu()
the menu where the recent files are kept.
|
RecentFileMenu.RecentFileEntry |
getMostRecent() |
void |
load(java.util.Properties p)
read the recent file names from the properties object.
|
void |
load(java.lang.String filename)
read the recent files from the given properties file
|
void |
setMaxNumberOfEntries(int max)
specify the maximal number of recent files in the list.
|
void |
store(java.util.Properties p)
Put the names of the recent Files into the properties object.
|
void |
store(java.lang.String filename)
write the recent file names to the given properties file.
|
public RecentFileMenu(KeYMediator mediator)
listener
- the ActionListener that will be notified of the user
clicked on a recent file menu entry. The selected filename can be
determined with the ActionEvent's getSource() method, cast the Object
into a JMenuItem and call the getLabel() method.maxNumberOfEntries
- the maximal number of items/entries in the
recent file menu.p
- a Properties object containing information about the recent
files to be displayed initially.
Or null
to use no initial information.public java.lang.String getAbsolutePath(javax.swing.JMenuItem item)
public void addRecentFile(java.lang.String name)
setMaxNumberOfEntries(int i)
method).name
- the name of the file.public void setMaxNumberOfEntries(int max)
public javax.swing.JMenu getMenu()
public void load(java.util.Properties p)
public void store(java.util.Properties p)
public final void load(java.lang.String filename)
public RecentFileMenu.RecentFileEntry getMostRecent()
public void store(java.lang.String filename)
Copyright © 2003-2019 The KeY-Project.