Adding JMCR-Stable version
[Benchmarks_CSolver.git] / JMCR-Stable / real-world application / jigsaw / src / org / w3c / www / http / headerEnumerator.java
diff --git a/JMCR-Stable/real-world application/jigsaw/src/org/w3c/www/http/headerEnumerator.java b/JMCR-Stable/real-world application/jigsaw/src/org/w3c/www/http/headerEnumerator.java
new file mode 100644 (file)
index 0000000..d98ab34
--- /dev/null
@@ -0,0 +1,64 @@
+// headerEnumerator.java\r
+// $Id: headerEnumerator.java,v 1.1 2010/06/15 12:19:49 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.www.http;\r
+\r
+import java.util.Dictionary;\r
+import java.util.Enumeration;\r
+import java.util.Hashtable;\r
+import java.util.NoSuchElementException;\r
+\r
+class headerEnumerator implements Enumeration {\r
+    HttpMessage message = null;\r
+    int         index   = 0;\r
+    Enumeration extras  = null;\r
+    boolean     all     = false;\r
+\r
+    /**\r
+     * Are there more available header descriptions ?\r
+     * @return A boolean, <strong>true</strong> if more header descriptions\r
+     * are available.\r
+     */\r
+\r
+    public boolean hasMoreElements() {\r
+       // Enumerate standard header descriptions:\r
+       while ( index < HttpMessage.MAX_HEADERS ) {\r
+           if (all || message.values[index] != null )\r
+               return true;\r
+           index++;\r
+       }\r
+       // Enumerate extra header descriptions:\r
+       if ( extras == null ) {\r
+           if ( message.headers == null ) \r
+               return false;\r
+           if ( all )\r
+               extras = message.factory.keys();\r
+           else\r
+               extras = message.headers.keys();\r
+       }\r
+       return extras.hasMoreElements();\r
+    }\r
+\r
+    /**\r
+     * Get the next header description out of this enumeration.\r
+     * @return A HeaderDescription.\r
+     * @exception NoSuchElement If no more header descriptions are available.\r
+     */\r
+\r
+    public Object nextElement() {\r
+       if ( index < HttpMessage.MAX_HEADERS )\r
+           return message.descriptors[index++];\r
+       if ( extras == null )\r
+           throw new NoSuchElementException("Enumeration exhausted.");\r
+       String key = (String) extras.nextElement();\r
+       return message.factory.get(key);\r
+    }\r
+\r
+    headerEnumerator(HttpMessage message, boolean all) {\r
+       this.message = message;\r
+       this.index   = 0;\r
+       this.all     = all;\r
+    }\r
+}\r