diff -r e4d514f81d95 -r 75e6b9dd5336 src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Wed Jul 11 12:23:34 2007 +0200
+++ b/src/Pure/General/url.ML	Wed Jul 11 17:47:45 2007 +0200
@@ -53,11 +53,11 @@
 local
 
 val scan_host =
-  (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
+  (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --|
   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
 
-val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
-val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
+val scan_path = Scan.many Symbol.is_regular >> (Path.explode o implode);
+val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode o implode o cons "/");
 
 val scan_url =
   Scan.unless (Scan.this_string "file:" ||