improved RemoteFile;
authorwenzelm
Thu Jun 10 20:12:49 2004 +0200 (2004-06-10 ago)
changeset 149189f30a1238090
parent 14917 b54b11ebe220
child 14919 0f5fde03e2b5
improved RemoteFile;
src/Pure/General/url.ML
     1.1 --- a/src/Pure/General/url.ML	Thu Jun 10 20:11:51 2004 +0200
     1.2 +++ b/src/Pure/General/url.ML	Thu Jun 10 20:12:49 2004 +0200
     1.3 @@ -51,16 +51,27 @@
     1.4  
     1.5  (* unpack *)
     1.6  
     1.7 +local
     1.8 +
     1.9 +fun gen_host quant = (quant (not_equal "/" andf Symbol.not_eof) >> implode) --|
    1.10 +  Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
    1.11 +
    1.12 +val scan_host = gen_host Scan.any;
    1.13 +val scan_host1 = gen_host Scan.any1;
    1.14  val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
    1.15 -val scan_host = Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode;
    1.16  
    1.17  val scan_url =
    1.18    Scan.unless (Scan.this_string "file:" ||
    1.19      Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
    1.20 -  Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile ||
    1.21 -  Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
    1.22 -  Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
    1.23 +  Scan.this_string "file://" |--
    1.24 +    (scan_host >> (fn "localhost" => "" | h => h)) -- scan_path >> RemoteFile ||
    1.25 +  Scan.this_string "http://" |-- scan_host1 -- scan_path >> Http ||
    1.26 +  Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp;
    1.27 +
    1.28 +in
    1.29  
    1.30  fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
    1.31  
    1.32  end;
    1.33 +
    1.34 +end;