src/Pure/General/url.ML
changeset 15174 fff9c761f89e
parent 14981 e73f8140af78
child 15175 b62f7b493360
     1.1 --- a/src/Pure/General/url.ML	Fri Sep 03 00:26:18 2004 +0200
     1.2 +++ b/src/Pure/General/url.ML	Fri Sep 03 00:28:44 2004 +0200
     1.3 @@ -55,15 +55,15 @@
     1.4  fun gen_host quant = (quant (not_equal "/" andf Symbol.not_eof) >> implode) --|
     1.5    Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
     1.6  
     1.7 -val scan_host = gen_host Scan.any;
     1.8  val scan_host1 = gen_host Scan.any1;
     1.9  val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
    1.10  
    1.11  val scan_url =
    1.12    Scan.unless (Scan.this_string "file:" ||
    1.13      Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
    1.14 -  Scan.this_string "file://" |--
    1.15 -    (scan_host >> (fn "localhost" => "" | h => h)) -- scan_path >> RemoteFile ||
    1.16 +  Scan.this_string "file:///" |-- scan_path >> File ||
    1.17 +  Scan.this_string "file://localhost/" |-- scan_path >> File ||
    1.18 +  Scan.this_string "file://" |-- scan_host1 -- scan_path >> RemoteFile ||
    1.19    Scan.this_string "http://" |-- scan_host1 -- scan_path >> Http ||
    1.20    Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp;
    1.21