|
1
22
23 package org.gjt.sp.jedit;
24
25 import java.io.*;
27 import java.util.*;
28
29 import org.xml.sax.InputSource  ;
30 import org.xml.sax.helpers.DefaultHandler ;
31
32 import org.gjt.sp.jedit.msg.DynamicMenuChanged;
33 import org.gjt.sp.jedit.textarea.*;
34 import org.gjt.sp.util.Log;
35 import org.gjt.sp.util.XMLUtilities;
36
38
43 public class BufferHistory
44 {
45 public static Entry getEntry(String path)
47 {
48 Iterator iter = history.iterator();
49 while(iter.hasNext())
50 {
51 Entry entry = (Entry)iter.next();
52 if(MiscUtilities.pathsEqual(entry.path,path))
53 return entry;
54 }
55
56 return null;
57 }
59 public static void setEntry(String path, int caret, Selection[] selection,
61 String encoding)
62 {
63 removeEntry(path);
64 addEntry(new Entry(path,caret,selectionToString(selection),
65 encoding));
66 EditBus.send(new DynamicMenuChanged("recent-files"));
67 }
69
74 public static void clear()
75 {
76 history.clear();
77 EditBus.send(new DynamicMenuChanged("recent-files"));
78 }
80
84 public static List getHistory()
85 {
86 return history;
87 }
89 public static void load()
91 {
92 String settingsDirectory = jEdit.getSettingsDirectory();
93 if(settingsDirectory == null)
94 return;
95
96 File recent = new File(MiscUtilities.constructPath(
97 settingsDirectory,"recent.xml"));
98 if(!recent.exists())
99 return;
100
101 recentModTime = recent.lastModified();
102
103 Log.log(Log.MESSAGE,BufferHistory.class,"Loading recent.xml");
104
105 RecentHandler handler = new RecentHandler();
106 try
107 {
108 XMLUtilities.parseXML(new FileInputStream(recent), handler);
109 }
110 catch(IOException e)
111 {
112 Log.log(Log.ERROR,BufferHistory.class,e);
113 }
114 }
116 public static void save()
118 {
119 String settingsDirectory = jEdit.getSettingsDirectory();
120 if(settingsDirectory == null)
121 return;
122
123 File file1 = new File(MiscUtilities.constructPath(
124 settingsDirectory, "#recent.xml#save#"));
125 File file2 = new File(MiscUtilities.constructPath(
126 settingsDirectory, "recent.xml"));
127 if(file2.exists() && file2.lastModified() != recentModTime)
128 {
129 Log.log(Log.WARNING,BufferHistory.class,file2
130 + " changed on disk; will not save recent"
131 + " files");
132 return;
133 }
134
135 jEdit.backupSettingsFile(file2);
136
137 Log.log(Log.MESSAGE,BufferHistory.class,"Saving " + file1);
138
139 String lineSep = System.getProperty("line.separator");
140
141 boolean ok = false;
142
143 BufferedWriter out = null;
144
145 try
146 {
147 out = new BufferedWriter(new FileWriter(file1));
148
149 out.write("<?xml version=\"1.0\"?>");
150 out.write(lineSep);
151 out.write("<!DOCTYPE RECENT SYSTEM \"recent.dtd\">");
152 out.write(lineSep);
153 out.write("<RECENT>");
154 out.write(lineSep);
155
156 Iterator iter = history.iterator();
157 while(iter.hasNext())
158 {
159 out.write("<ENTRY>");
160 out.write(lineSep);
161
162 Entry entry = (Entry)iter.next();
163
164 out.write("<PATH>");
165 out.write(XMLUtilities.charsToEntities(entry.path,false));
166 out.write("</PATH>");
167 out.write(lineSep);
168
169 out.write("<CARET>");
170 out.write(String.valueOf(entry.caret));
171 out.write("</CARET>");
172 out.write(lineSep);
173
174 if(entry.selection != null
175 && entry.selection.length() > 0)
176 {
177 out.write("<SELECTION>");
178 out.write(entry.selection);
179 out.write("</SELECTION>");
180 out.write(lineSep);
181 }
182
183 if(entry.encoding != null)
184 {
185 out.write("<ENCODING>");
186 out.write(entry.encoding);
187 out.write("</ENCODING>");
188 out.write(lineSep);
189 }
190
191 out.write("</ENTRY>");
192 out.write(lineSep);
193 }
194
195 out.write("</RECENT>");
196 out.write(lineSep);
197
198 out.close();
199
200 ok = true;
201 }
202 catch(Exception e)
203 {
204 Log.log(Log.ERROR,BufferHistory.class,e);
205 }
206 finally
207 {
208 try
209 {
210 if(out != null)
211 out.close();
212 }
213 catch(IOException e)
214 {
215 }
216 }
217
218 if(ok)
219 {
220
222 file2.delete();
223 file1.renameTo(file2);
224 }
225
226 recentModTime = file2.lastModified();
227 }
229 private static LinkedList history;
231 private static long recentModTime;
232
233 static
235 {
236 history = new LinkedList();
237 }
239 static void addEntry(Entry entry)
241 {
242 history.addFirst(entry);
243 int max = jEdit.getIntegerProperty("recentFiles",50);
244 while(history.size() > max)
245 history.removeLast();
246 }
248 static void removeEntry(String path)
250 {
251 Iterator iter = history.iterator();
252 while(iter.hasNext())
253 {
254 Entry entry = (Entry)iter.next();
255 if(MiscUtilities.pathsEqual(path,entry.path))
256 {
257 iter.remove();
258 return;
259 }
260 }
261 }
263 private static String selectionToString(Selection[] s)
265 {
266 if(s == null)
267 return null;
268
269 StringBuffer buf = new StringBuffer ();
270
271 for(int i = 0; i < s.length; i++)
272 {
273 if(i != 0)
274 buf.append(' ');
275
276 Selection sel = s[i];
277 if(sel instanceof Selection.Range)
278 buf.append("range ");
279 else buf.append("rect ");
281 buf.append(sel.getStart());
282 buf.append(' ');
283 buf.append(sel.getEnd());
284 }
285
286 return buf.toString();
287 }
289 private static Selection[] stringToSelection(String s)
291 {
292 if(s == null)
293 return null;
294
295 Vector selection = new Vector();
296 StringTokenizer st = new StringTokenizer(s);
297
298 while(st.hasMoreTokens())
299 {
300 String type = st.nextToken();
301 int start = Integer.parseInt(st.nextToken());
302 int end = Integer.parseInt(st.nextToken());
303 if(end < start)
304 {
305 continue;
309 }
310
311 Selection sel;
312 if(type.equals("range"))
313 sel = new Selection.Range(start,end);
314 else sel = new Selection.Rect(start,end);
316
317 selection.addElement(sel);
318 }
319
320 Selection[] returnValue = new Selection[selection.size()];
321 selection.copyInto(returnValue);
322 return returnValue;
323 }
325
327
331 public static class Entry
332 {
333 public String path;
334 public int caret;
335 public String selection;
336 public String encoding;
337
338 public Selection[] getSelection()
339 {
340 return stringToSelection(selection);
341 }
342
343 public Entry(String path, int caret, String selection, String encoding)
344 {
345 this.path = path;
346 this.caret = caret;
347 this.selection = selection;
348 this.encoding = encoding;
349 }
350
351 public String toString()
352 {
353 return path + ": " + caret;
354 }
355 }
357 static class RecentHandler extends DefaultHandler
359 {
360 public void endDocument()
361 {
362 int max = jEdit.getIntegerProperty("recentFiles",50);
363 while(history.size() > max)
364 history.removeLast();
365 }
366
367 public InputSource resolveEntity(String publicId, String systemId)
368 {
369 return XMLUtilities.findEntity(systemId, "recent.dtd", getClass());
370 }
371
372 public void endElement(String uri, String localName, String name)
373 {
374 if(name.equals("ENTRY"))
375 {
376 history.addLast(new Entry(
377 path,caret,selection,
378 encoding));
379 path = null;
380 caret = 0;
381 selection = null;
382 encoding = null;
383 }
384 else if(name.equals("PATH"))
385 path = charData.toString();
386 else if(name.equals("CARET"))
387 caret = Integer.parseInt(charData.toString());
388 else if(name.equals("SELECTION"))
389 selection = charData.toString();
390 else if(name.equals("ENCODING"))
391 encoding = charData.toString();
392 charData.setLength(0);
393 }
394
395 public void characters(char[] ch, int start, int length)
396 {
397 charData.append(ch,start,length);
398 }
399
400
402 private String path;
404 private int caret;
405 private String selection;
406 private String encoding;
407 private StringBuffer charData = new StringBuffer ();
408 } }
410 |
Popular Tags |
Java API By Example, From Geeks To Geeks.