diff -r f8715e7c1be6 -r b979c781c2db src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/General/url.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -54,11 +54,11 @@
 local
 
 val scan_host =
-  (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --|
+  (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
 
-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_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_url =
   Scan.unless (Scan.this_string "file:" ||