src/Pure/General/url.ML
changeset 15625 43f1669cbae3
parent 15175 b62f7b493360
child 15627 7a108ae4c798
     1.1 --- a/src/Pure/General/url.ML	Thu Mar 24 17:03:37 2005 +0100
     1.2 +++ b/src/Pure/General/url.ML	Fri Mar 25 13:03:47 2005 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Basic URLs.
     1.8 +Basic URLs.  See RFC 1738.
     1.9  *)
    1.10  
    1.11  signature URL =
    1.12 @@ -66,7 +66,10 @@
    1.13    Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
    1.14    Scan.this_string "file://" |-- scan_host1 -- scan_path >> RemoteFile ||
    1.15    Scan.this_string "http://" |-- scan_host1 -- scan_path >> Http ||
    1.16 -  Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp;
    1.17 +  Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp ||
    1.18 +  Scan.this_string "file://" |-- scan_host1 -- scan_path >> Ftp (* or other proto *) ||
    1.19 +  (* NB: this next one is not in RFC 1738, but produced by some Haskell libraries *)
    1.20 +  Scan.this_string "file:" |-- scan_path >> File 
    1.21  
    1.22  in
    1.23