src/Pure/General/url.ML
author wenzelm
Fri Dec 14 11:52:54 2001 +0100 (2001-12-14)
changeset 12498 3b0091bf06e8
parent 8806 a202293db3f6
child 14909 988b4342ed1f
permissions -rw-r--r--
changed Thm.varifyT';
     1 (*  Title:      Pure/General/url.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Basic URLs.
     7 *)
     8 
     9 signature URL =
    10 sig
    11   type T
    12   val file: Path.T -> T
    13   val http: string * Path.T -> T
    14   val ftp: string * Path.T -> 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 
    24 (* type url *)
    25 
    26 datatype scheme = File | Http of string | Ftp of string;
    27 
    28 datatype T = Url of scheme * Path.T;
    29 
    30 fun file p = Url (File, p);
    31 fun http (h, p) = Url (Http h, p);
    32 fun ftp (h, p) = Url (Ftp h, p);
    33 
    34 
    35 (* append *)
    36 
    37 fun append (Url (s, p)) (Url (File, p')) = Url (s, Path.append p p')
    38   | append _ url = url;
    39 
    40 
    41 (* pack *)
    42 
    43 fun pack_scheme File = ""
    44   | pack_scheme (Http host) = "http://" ^ host
    45   | pack_scheme (Ftp host) = "ftp://" ^ host;
    46 
    47 fun pack (Url (s, p)) = pack_scheme s ^ (if Path.is_current p then "" else Path.pack p);
    48 
    49 
    50 (* unpack *)
    51 
    52 fun scan_lits [] x = ("", x)
    53   | scan_lits (c :: cs) x = (($$ c -- scan_lits cs) >> op ^) x;
    54 
    55 val scan_literal = scan_lits o Symbol.explode;
    56 
    57 val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
    58 val scan_host = Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode;
    59 
    60 val scan_url =
    61   scan_literal "http://" |-- scan_host -- scan_path >> http ||
    62   scan_literal "ftp://" |-- scan_host -- scan_path >> ftp ||
    63   Scan.unless (scan_literal "http:" || scan_literal "ftp:") scan_path >> file;
    64 
    65 fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
    66 
    67 
    68 end;