public class RecentFileMenu
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
RecentFileMenu.RecentFileEntry |
Modifier and Type | Field and Description |
---|---|
private java.awt.event.ActionListener |
lissy
the actionListener to be notified of mouse-clicks or other actionevents
on the menu items
|
private static int |
MAX_RECENT_FILES
The maximum number of recent files displayed.
|
private int |
maxNumberOfEntries
this is the maximal number of recent files.
|
private javax.swing.JMenu |
menu |
private RecentFileMenu.RecentFileEntry |
mostRecentFile |
private java.util.HashMap<javax.swing.JMenuItem,RecentFileMenu.RecentFileEntry> |
recentFiles
list of recent files
|
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.
|
private void |
addToModelAndView(java.lang.String name)
add file name to the menu
|
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
|
private void |
removeFromModelAndView(javax.swing.JMenuItem item,
int index) |
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.
|
private static final int MAX_RECENT_FILES
private int maxNumberOfEntries
private javax.swing.JMenu menu
private java.awt.event.ActionListener lissy
private java.util.HashMap<javax.swing.JMenuItem,RecentFileMenu.RecentFileEntry> recentFiles
private RecentFileMenu.RecentFileEntry mostRecentFile
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.private void removeFromModelAndView(javax.swing.JMenuItem item, int index)
private void addToModelAndView(java.lang.String name)
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)