001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: // This file is part of KeY - Integrated Deductive Software Design
010: // Copyright (C) 2001-2004 Universitaet Karlsruhe, Germany
011: // Universitaet Koblenz-Landau, Germany
012: // Chalmers University of Technology, Sweden
013: //
014: // The KeY system is protected by the GNU General Public License.
015: // See LICENSE.TXT for details.
016: package de.uka.ilkd.key.gui;
017:
018: import java.awt.event.ActionListener;
019: import java.io.*;
020: import java.util.Enumeration;
021: import java.util.HashMap;
022: import java.util.Properties;
023:
024: import javax.swing.JMenu;
025: import javax.swing.JMenuItem;
026:
027: import de.uka.ilkd.key.util.Debug;
028:
029: /**
030: * This class offers a mechanism to manage recent files; it adds the
031: * necessary menu items to a menu or even can provide that menu itself.
032: * also it offers a way to read the recent files from a java.util.Properties
033: * object and can store them again to a Properties object.
034: * This class is a result of the fusion of the RecentFileBuffer and RecentFiles
035: * classes.
036: * It's not a Menu in itself!!!
037: * @author Ute Platzer, with a lot of input from Volker Braun.
038: */
039: public class RecentFileMenu {
040:
041: /** this is the maximal number of recent files. */
042: private int maxNumberOfEntries;
043:
044: private JMenu menu;
045:
046: /** the actionListener to be notified of mouse-clicks or other actionevents
047: * on the menu items */
048: private ActionListener lissy;
049:
050: /**
051: * list of recent files
052: */
053: private HashMap recentFiles;
054:
055: private RecentFileEntry mostRecentFile;
056:
057: /**
058: * Create a new RecentFiles list.
059: * @param listener the ActionListener that will be notified of the user
060: * clicked on a recent file menu entry. The selected filename can be
061: * determined with the ActionEvent's getSource() method, cast the Object
062: * into a JMenuItem and call the getLabel() method.
063: * @param maxNumberOfEntries the maximal number of items/entries in the
064: * recent file menu.
065: * @param p a Properties object containing information about the recent
066: * files to be displayed initially.
067: * Or <code>null</code> to use no initial information.
068: */
069: public RecentFileMenu(ActionListener listener,
070: int maxNumberOfEntries, Properties p) {
071: this .menu = new JMenu("Recent Files");
072:
073: this .lissy = listener;
074: this .maxNumberOfEntries = maxNumberOfEntries;
075:
076: this .recentFiles = new HashMap();
077:
078: if (p != null)
079: load(p);
080:
081: menu.setEnabled(menu.getItemCount() != 0);
082:
083: }
084:
085: /**
086: */
087: private void removeFromModelAndView(JMenuItem item, int index) {
088: recentFiles.remove(item);
089: menu.remove(index);
090: }
091:
092: /**
093: * add file name to the menu
094: */
095: private void addToModelAndView(final String name) {
096: final RecentFileEntry entry = new RecentFileEntry(name);
097: if (new File(entry.getAbsolutePath()).exists()) {
098: JMenuItem item = new JMenuItem(entry.getFileName());
099: item.setToolTipText(entry.getAbsolutePath());
100: recentFiles.put(item, entry);
101: item.addActionListener(lissy);
102: menu.insert(item, 0);
103: mostRecentFile = entry;
104: }
105: }
106:
107: /**
108: *
109: */
110: public String getAbsolutePath(JMenuItem item) {
111: return ((RecentFileEntry) recentFiles.get(item))
112: .getAbsolutePath();
113: }
114:
115: /**
116: * call this method to add a new file to the beginning of the RecentFiles
117: * list. If the name is already part of the list, it will be moved to the
118: * first position. No more than a specified maximum number of names will
119: * be allowed in the list, and additional names will be removed at the end.
120: * (set the maximum number with the {@link #setMaxNumberOfEntries(int i)} method).
121: * @param name the name of the file.
122: */
123: public void addRecentFile(final String name) {
124: //Add the name to the recentFileList:
125: //check whether this name is already there
126: Debug.out("recentfilemenu: add file: ", name);
127: Debug
128: .out("recentfilemenu: at menu count:", menu
129: .getItemCount());
130: int index = -1;
131: JMenuItem item = null;
132: for (int i = 0; i < menu.getItemCount(); i++) {
133: if (menu.getItem(i) == null) {
134: continue;
135: }
136: Debug.out("", i);
137: Debug.out("item is ", menu.getItem(i));
138: Debug.out("name is ", menu.getItem(i).getText());
139: if (((RecentFileEntry) recentFiles.get(menu.getItem(i)))
140: .getAbsolutePath().equals(name)) {
141: //this name has to be put at the first position
142: item = menu.getItem(i);
143: index = i;
144: break;
145: }
146: }
147:
148: if (index != -1) {
149: //move the name to the first position
150: removeFromModelAndView(item, index);
151: }
152: // if appropriate, remove the last entry.
153: if (menu.getItemCount() == maxNumberOfEntries) {
154: removeFromModelAndView(menu
155: .getItem(menu.getItemCount() - 1), menu
156: .getItemCount() - 1);
157: }
158: addToModelAndView(name);
159: menu.setEnabled(menu.getItemCount() != 0);
160: }
161:
162: /**
163: * specify the maximal number of recent files in the list.
164: * The default is 5
165: */
166: public void setMaxNumberOfEntries(int max) {
167: if (maxNumberOfEntries > max && menu.getItemCount() > max) {
168: for (int i = menu.getItemCount() - 1; i > max; i--) {
169: menu.remove(i);
170: }
171:
172: }
173: this .maxNumberOfEntries = max;
174: }
175:
176: /**
177: * the menu where the recent files are kept. If the user didn't specify
178: * one in the constructor, a new JMenu is created. It can be accessed
179: * via this method.
180: */
181: public JMenu getMenu() {
182: return menu;
183: }
184:
185: /**
186: * read the recent file names from the properties object.
187: * the property names are expected to be "RecentFile0" "RecentFile1" ...
188: */
189: public void load(Properties p) {
190: int i = maxNumberOfEntries;
191: String s = null;
192: do {
193: s = p.getProperty("RecentFile" + i);
194: if (s != null)
195: addRecentFile(s);
196: i--;
197: } while (i >= 0);
198: }
199:
200: /**
201: * Put the names of the recent Files into the properties object.
202: * The property names are "RecentFile0" "RecentFile1" ...
203: * The values are fully qualified path names.
204: */
205: public void store(Properties p) {
206: //if there's nothing to store:
207: for (int i = 0; i < menu.getItemCount(); i++) {
208: p.setProperty("RecentFile" + i, getAbsolutePath(menu
209: .getItem(i)));
210: }
211: }
212:
213: /** read the recent files from the given properties file */
214: public void load(String filename) {
215: try {
216: Properties p = new Properties();
217: p.load(new FileInputStream(filename));
218: Enumeration e = p.propertyNames();
219: while (e.hasMoreElements()) {
220: String s = (String) e.nextElement();
221: if (s.indexOf("RecentFile") != -1)
222: addRecentFile(p.getProperty(s));
223: }
224: } catch (FileNotFoundException ex) {
225: Debug
226: .out(
227: "Could not read RecentFileList. Did not find file ",
228: filename);
229: } catch (IOException ioe) {
230: Debug
231: .out(
232: "Could not read RecentFileList. Some IO Error occured ",
233: ioe);
234: }
235: }
236:
237: public RecentFileEntry getMostRecent() {
238: return mostRecentFile;
239: }
240:
241: /**
242: * write the recent file names to the given properties file.
243: * the file will be read (if it exists) and then re-written so no
244: * information will be lost.
245: */
246: public void store(String filename) {
247: File localRecentFiles = new File(filename);
248: FileInputStream fin;
249: FileOutputStream fout;
250: Properties p = new Properties();
251: try {
252: // creates a new file if it does not exist yet
253: localRecentFiles.createNewFile();
254:
255: fin = new FileInputStream(localRecentFiles);
256: fout = new FileOutputStream(localRecentFiles);
257: p.load(fin);
258: store(p);
259: p.store(fout, "recent files");
260: } catch (IOException ex) {
261: System.err.println("Cound not write recentFileList due to "
262: + ex.toString() + "::" + localRecentFiles);
263: }
264: }
265:
266: public static class RecentFileEntry {
267:
268: private String fileName;
269: private String absolutePath;
270:
271: public RecentFileEntry(String absolutePath) {
272: this .absolutePath = absolutePath;
273: int lastIndex = absolutePath
274: .lastIndexOf(File.separatorChar);
275:
276: this .fileName = (lastIndex == -1 ? absolutePath
277: : absolutePath.substring(lastIndex + 1,
278: absolutePath.length()));
279: }
280:
281: public String getAbsolutePath() {
282: return absolutePath;
283: }
284:
285: public String getFileName() {
286: return fileName;
287: }
288:
289: public String toString() {
290: return fileName;
291: }
292:
293: }
294:
295: }
|