[cp-patches] RFC: prevent URL degeneration

[Robert Schuster]

Hi all,
as chris supposed I tried to find another (and better) way of fixing the URL
class' toString problem which affects our XML parser.

To make a long story short. Consider the following code fragment:

u = new URL("file:////home/baz");

u2 = new URL(u.toString());

print(u2.toString());

print(u2.getHome());

On the JDK this will print

file://home/baz
home

(This happens on the JDK as well as with Classpath.)

Which is obviously not what file:////home/baz meant. The problem exists because
URL.toString() does not care about superfluous leading slashes. With the
attached patch Classpath will not have this problem anymore because superfluous
leading slashes are carefully removed. The output will be:

file:/home/baz
<empty string>

Fixes PR 24249.

2005-10-07  Robert Schuster  <address@hidden>

    * java/net/URLStreamHandler.java:
    (toExternalForm): Remove superfluous leading slashes from URL
    paths.

Ah yes. Please give me input about this patch. For me it fixes the problem with
the application I was debugging.

cu
Robert

Index: java/net/URLStreamHandler.java
===================================================================
RCS file: /cvsroot/classpath/classpath/java/net/URLStreamHandler.java,v
retrieving revision 1.35
diff -u -r1.35 URLStreamHandler.java
--- java/net/URLStreamHandler.java      2 Oct 2005 22:58:41 -0000       1.35
+++ java/net/URLStreamHandler.java      9 Oct 2005 20:48:59 -0000
@@ -520,6 +520,25 @@
        sb.append("//").append(authority);
       }
 
+    // If we have superfluous leading slashes (that means, at least 2)
+    // we subsequently remove them and add a filepath with only one
+    // slash. In case that the filepath had none or one slash it is
+    // appended unchanged.
+    // By doing this we prevent that an URL with many superfluous
+    // leading slashes in the filepath degenerates into an URL
+    // where parts of the path become the host. Without that code
+    // new URL(new URL("file:////home/foo").toString()) would result
+    // in an URL instance which points to file://home/foo .
+    if ( file.startsWith("//") )
+      {
+    int slash = 1;
+    while ( file.charAt(slash+1) == '/' )
+      {
+    slash++;
+      }
+    sb.append(file.substring(slash));
+      }
+    else
     sb.append(file);
 
     if (ref != null)