src/Pure/General/url.ML
changeset 6639 d399db16964c
child 8806 a202293db3f6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/url.ML	Wed May 12 16:51:52 1999 +0200
     1.3 @@ -0,0 +1,67 @@
     1.4 +(*  Title:      Pure/General/url.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Basic URLs.
     1.9 +*)
    1.10 +
    1.11 +signature URL =
    1.12 +sig
    1.13 +  type T
    1.14 +  val file: Path.T -> T
    1.15 +  val http: string * Path.T -> T
    1.16 +  val ftp: string * Path.T -> T
    1.17 +  val append: T -> T -> T
    1.18 +  val pack: T -> string
    1.19 +  val unpack: string -> T
    1.20 +end;
    1.21 +
    1.22 +structure Url: URL =
    1.23 +struct
    1.24 +
    1.25 +
    1.26 +(* type url *)
    1.27 +
    1.28 +datatype scheme = File | Http of string | Ftp of string;
    1.29 +
    1.30 +datatype T = Url of scheme * Path.T;
    1.31 +
    1.32 +fun file p = Url (File, p);
    1.33 +fun http (h, p) = Url (Http h, p);
    1.34 +fun ftp (h, p) = Url (Ftp h, p);
    1.35 +
    1.36 +
    1.37 +(* append *)
    1.38 +
    1.39 +fun append (Url (s, p)) (Url (File, p')) = Url (s, Path.append p p')
    1.40 +  | append _ url = url;
    1.41 +
    1.42 +
    1.43 +(* pack *)
    1.44 +
    1.45 +fun pack_scheme File = ""
    1.46 +  | pack_scheme (Http host) = "http://" ^ host
    1.47 +  | pack_scheme (Ftp host) = "ftp://" ^ host;
    1.48 +
    1.49 +fun pack (Url (s, p)) = pack_scheme s ^ (if Path.is_current p then "" else Path.pack p);
    1.50 +
    1.51 +
    1.52 +(* unpack *)
    1.53 +
    1.54 +fun scan_lits [] x = ("", x)
    1.55 +  | scan_lits (c :: cs) x = (($$ c -- scan_lits cs) >> op ^) x;
    1.56 +
    1.57 +val scan_literal = scan_lits o Symbol.explode;
    1.58 +
    1.59 +val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
    1.60 +val scan_host = Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode;
    1.61 +
    1.62 +val scan_url =
    1.63 +  scan_literal "http://" |-- scan_host -- scan_path >> http ||
    1.64 +  scan_literal "ftp://" |-- scan_host -- scan_path >> ftp ||
    1.65 +  Scan.unless (scan_literal "http:" || scan_literal "ftp:") scan_path >> file;
    1.66 +
    1.67 +fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
    1.68 +
    1.69 +
    1.70 +end;