145 |
// If encounter another "/", it's end of a null host part or beginning of root path |
// If encounter another "/", it's end of a null host part or beginning of root path |
146 |
if ( url_string.startsWith("/") ){ |
if ( url_string.startsWith("/") ){ |
147 |
hostpart = false; |
hostpart = false; |
148 |
url_string = url_string.substring(1); |
// url_string = url_string.substring(1); |
149 |
} |
} |
150 |
} |
} |
151 |
|
|
251 |
toExternalForm(URL url) |
toExternalForm(URL url) |
252 |
{ |
{ |
253 |
StringBuffer sb = new StringBuffer(PlatformHelper.INITIAL_MAX_PATH); |
StringBuffer sb = new StringBuffer(PlatformHelper.INITIAL_MAX_PATH); |
254 |
sb.append("file://"); |
sb.append("file:"); |
255 |
|
|
256 |
String prefix = url.getHost(); |
String prefix = url.getHost(); |
257 |
if(prefix != null && prefix.length() > 0){ |
if(prefix != null && prefix.length() > 0){ |