src/Pure/General/url.ML
changeset 16195 0eb3c15298cd
parent 15627 7a108ae4c798
child 19305 5c16895d548b
     1.1 --- a/src/Pure/General/url.ML	Thu Jun 02 18:29:54 2005 +0200
     1.2 +++ b/src/Pure/General/url.ML	Thu Jun 02 18:29:55 2005 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Basic URLs.  See RFC 1738.
     1.8 +Basic URLs, see RFC 1738.
     1.9  *)
    1.10  
    1.11  signature URL =
    1.12 @@ -52,22 +52,21 @@
    1.13  
    1.14  local
    1.15  
    1.16 -fun gen_host quant = (quant (not_equal "/" andf Symbol.not_eof) >> implode) --|
    1.17 +val scan_host =
    1.18 +  (Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode) --|
    1.19    Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
    1.20  
    1.21 -val scan_host1 = gen_host Scan.any1;
    1.22  val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
    1.23 -val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o (curry (op^) "/") o implode);
    1.24 +val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o implode o cons "/");
    1.25  
    1.26  val scan_url =
    1.27    Scan.unless (Scan.this_string "file:" ||
    1.28      Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
    1.29    Scan.this_string "file:///" |-- scan_path_root >> File ||
    1.30    Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
    1.31 -  Scan.this_string "file://" |-- scan_host1 -- scan_path >> RemoteFile ||
    1.32 -  Scan.this_string "http://" |-- scan_host1 -- scan_path >> Http ||
    1.33 -  Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp ||
    1.34 -  Scan.this_string "file://" |-- scan_host1 -- scan_path >> Ftp (* or other proto *)
    1.35 +  Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile ||
    1.36 +  Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
    1.37 +  Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
    1.38  
    1.39  in
    1.40