--- 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:" ||