Adding JMCR-Stable version

[Benchmarks_CSolver.git] / JMCR-Stable / real-world application / jigsaw / src / org / w3c / tools / resources / DateAttribute.java

diff --git a/JMCR-Stable/real-world application/jigsaw/src/org/w3c/tools/resources/DateAttribute.java b/JMCR-Stable/real-world application/jigsaw/src/org/w3c/tools/resources/DateAttribute.java
new file mode 100644 (file)
index 0000000..6f1c7dd
--- /dev/null
+++ b/JMCR-Stable/real-world application/jigsaw/src/org/w3c/tools/resources/DateAttribute.java
@@ -0,0 +1,76 @@
+// DateAttribute.java\r
+// $Id: DateAttribute.java,v 1.1 2010/06/15 12:20:14 smhuang Exp $\r
+// (c) COPYRIGHT MIT and INRIA, 1996.\r
+// Please first read the full copyright statement in file COPYRIGHT.html\r
+\r
+package org.w3c.tools.resources ;\r
+\r
+import java.text.SimpleDateFormat;\r
+import java.text.ParseException;\r
+import java.util.Date;\r
+import java.util.TimeZone;\r
+\r
+public class DateAttribute extends LongAttribute {\r
+\r
+    String cachedPickledValue = null;\r
+    Long   cachedPickledLong = null;\r
+\r
+    public DateAttribute(String name, Object def, int flags) {\r
+       super(name, (Long) def, flags) ;\r
+       this.type = "java.util.Date".intern();\r
+    }\r
+\r
+    public DateAttribute() {\r
+       super();\r
+    }\r
+\r
+    /**\r
+     * Get a DateFormat compliant with RFC 822 updated by RFC 1123.\r
+     * @return a SimpleDateFormat instance.\r
+     */\r
+    private SimpleDateFormat getDateFormatter() {\r
+       SimpleDateFormat formatter = \r
+           new SimpleDateFormat("EEE, dd MMM yyyy HH:mm:ss zzz");\r
+       formatter.setTimeZone(TimeZone.getTimeZone("GMT"));\r
+       return formatter;\r
+    }\r
+\r
+    /**\r
+     * Pickle an integer to the given output stream.\r
+     * @param obj The object to pickle.\r
+     * @exception IOException If some IO error occured.\r
+     */\r
+\r
+    public String pickle(Object obj) {\r
+       if (obj == cachedPickledLong) {\r
+           if (cachedPickledValue == null) {\r
+               SimpleDateFormat formatter = getDateFormatter();\r
+               String s = formatter.format(new Date(((Long)obj).longValue()));\r
+               cachedPickledValue = s;\r
+               return s;\r
+           }\r
+           return cachedPickledValue;\r
+       }\r
+       SimpleDateFormat formatter = getDateFormatter();\r
+       return formatter.format(new Date(((Long)obj).longValue()));\r
+    }\r
+\r
+    /**\r
+     * Unpickle an integer from the given input stream.\r
+     * @param value the string representation of this integer\r
+     * @return An instance of Integer.\r
+     * @exception IOException If some IO error occured.\r
+     */\r
+\r
+    public Object unpickle (String value) {\r
+       try {\r
+           SimpleDateFormat formatter = getDateFormatter();\r
+           Long l = new Long((formatter.parse(value)).getTime());\r
+           cachedPickledLong = l;\r
+           return l;\r
+       } catch (ParseException ex) {\r
+           return new Long(-1);\r
+       }\r
+    }\r
+\r
+}\r