src/Pure/General/url.ML
author aspinall
Fri Mar 25 14:14:01 2005 +0100 (2005-03-25 ago)
changeset 15627 7a108ae4c798
parent 15625 43f1669cbae3
child 16195 0eb3c15298cd
permissions -rw-r--r--
Revert previous change (but leave comments).
     1 (*  Title:      Pure/General/url.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Basic URLs.  See RFC 1738.
     6 *)
     7 
     8 signature URL =
     9 sig
    10   datatype T =
    11     File of Path.T |
    12     RemoteFile of string * Path.T |
    13     Http of string * Path.T |
    14     Ftp of string * Path.T
    15   val append: T -> T -> T
    16   val pack: T -> string
    17   val unpack: string -> T
    18 end;
    19 
    20 structure Url: URL =
    21 struct
    22 
    23 (* type url *)
    24 
    25 datatype T =
    26   File of Path.T |
    27   RemoteFile of string * Path.T |
    28   Http of string * Path.T |
    29   Ftp of string * Path.T;
    30 
    31 
    32 (* append *)
    33 
    34 fun append (File p)            (File p') = File (Path.append p p')
    35   | append (RemoteFile (h, p)) (File p') = RemoteFile (h, Path.append p p')
    36   | append (Http (h, p))       (File p') = Http (h, Path.append p p')
    37   | append (Ftp (h, p))        (File p') = Ftp (h, Path.append p p')
    38   | append _ url = url;
    39 
    40 
    41 (* pack *)
    42 
    43 fun pack_path p = if Path.is_current p then "" else Path.pack p;
    44 
    45 fun pack (File p) = pack_path p
    46   | pack (RemoteFile (h, p)) = "file://" ^ h ^ pack_path p
    47   | pack (Http (h, p)) = "http://" ^ h ^ pack_path p
    48   | pack (Ftp (h, p)) = "ftp://" ^ h ^ pack_path p;
    49 
    50 
    51 (* unpack *)
    52 
    53 local
    54 
    55 fun gen_host quant = (quant (not_equal "/" andf Symbol.not_eof) >> implode) --|
    56   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
    57 
    58 val scan_host1 = gen_host Scan.any1;
    59 val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
    60 val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o (curry (op^) "/") o implode);
    61 
    62 val scan_url =
    63   Scan.unless (Scan.this_string "file:" ||
    64     Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
    65   Scan.this_string "file:///" |-- scan_path_root >> File ||
    66   Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
    67   Scan.this_string "file://" |-- scan_host1 -- scan_path >> RemoteFile ||
    68   Scan.this_string "http://" |-- scan_host1 -- scan_path >> Http ||
    69   Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp ||
    70   Scan.this_string "file://" |-- scan_host1 -- scan_path >> Ftp (* or other proto *)
    71 
    72 in
    73 
    74 fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
    75 
    76 end;
    77 
    78 end;