+ Server() {
+ if(!SERIALIZATION_DIR.equals("")) {
+ log("Looking for serialized stylesheets");
+ File [] serialized = new File(SERIALIZATION_DIR).listFiles();
+ if (serialized == null) {
+ log("Serialized stylesheets directory \"" + SERIALIZATION_DIR +
+ "\" not found");
+ } else {
+ for (int i = 0; i < serialized.length ; i++) {
+ File filename = serialized[i];
+ String key = filename.getName();
+ log("Found serialized stylesheet " + key);
+ log("Reloading serialized stylesheet \"" + filename + "\"... ");
+ FileInputStream istream;
+ try {
+ istream = new FileInputStream(filename);
+ ObjectInputStream p = new ObjectInputStream(istream);
+ Style style = (Style)p.readObject();
+ istream.close();
+ hashMap.put(key, style);
+ } catch (Exception e) {log(e.toString());};
+ }
+ log("Serialized stylesheets loaded!");
+ }
+ } else
+ log("Stylesheet serialization is off. Set the property SERIALIZATION_DIR to a non-empty value to turn it on.");
+
+ }
+