--- a/src/Pure/General/url.ML Fri Sep 03 00:28:44 2004 +0200
+++ b/src/Pure/General/url.ML Fri Sep 03 00:35:38 2004 +0200
@@ -57,12 +57,13 @@
val scan_host1 = gen_host Scan.any1;
val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
+val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o (curry (op^) "/") o implode);
val scan_url =
Scan.unless (Scan.this_string "file:" ||
Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
- Scan.this_string "file:///" |-- scan_path >> File ||
- Scan.this_string "file://localhost/" |-- scan_path >> File ||
+ Scan.this_string "file:///" |-- scan_path_root >> File ||
+ Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
Scan.this_string "file://" |-- scan_host1 -- scan_path >> RemoteFile ||
Scan.this_string "http://" |-- scan_host1 -- scan_path >> Http ||
Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp;