# HG changeset patch
# User wenzelm
# Date 1086891169 -7200
# Node ID 9f30a1238090771c0b89b8789ac328abdbec3871
# Parent  b54b11ebe22022ab28085b71e438ed03d22b167e
improved RemoteFile;

diff -r b54b11ebe220 -r 9f30a1238090 src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Thu Jun 10 20:11:51 2004 +0200
+++ b/src/Pure/General/url.ML	Thu Jun 10 20:12:49 2004 +0200
@@ -51,16 +51,27 @@
 
 (* unpack *)
 
+local
+
+fun gen_host quant = (quant (not_equal "/" andf Symbol.not_eof) >> implode) --|
+  Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
+
+val scan_host = gen_host Scan.any;
+val scan_host1 = gen_host Scan.any1;
 val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
-val scan_host = Scan.any1 (not_equal "/" andf Symbol.not_eof) >> 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_host -- scan_path >> RemoteFile ||
-  Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
-  Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
+  Scan.this_string "file://" |--
+    (scan_host >> (fn "localhost" => "" | h => h)) -- scan_path >> RemoteFile ||
+  Scan.this_string "http://" |-- scan_host1 -- scan_path >> Http ||
+  Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp;
+
+in
 
 fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
 
 end;
+
+end;