src/Pure/General/url.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23784 75e6b9dd5336
child 29606 fedb8be05f24
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/General/url.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Basic URLs, see RFC 1738 and RFC 2396.
     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 implode: T -> string
    17   val explode: 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 (* implode *)
    42 
    43 fun implode_path p = if Path.is_current p then "" else Path.implode p;
    44 
    45 fun implode_url (File p) = implode_path p
    46   | implode_url (RemoteFile (h, p)) = "file://" ^ h ^ implode_path p
    47   | implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
    48   | implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
    49 
    50 
    51 (* explode *)
    52 
    53 local
    54 
    55 val scan_host =
    56   (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --|
    57   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
    58 
    59 val scan_path = Scan.many Symbol.is_regular >> (Path.explode o implode);
    60 val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode o implode o cons "/");
    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_host -- scan_path >> RemoteFile ||
    68   Scan.this_string "file:/" |-- scan_path_root >> File ||
    69   Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
    70   Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
    71 
    72 in
    73 
    74 fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
    75 
    76 end;
    77 
    78 
    79 (*final declarations of this structure!*)
    80 val implode = implode_url;
    81 val explode = explode_url;
    82 
    83 end;