src/Pure/General/url.ML
author wenzelm
Wed May 12 16:51:52 1999 +0200 (1999-05-12 ago)
changeset 6639 d399db16964c
child 8806 a202293db3f6
permissions -rw-r--r--
Basic URLs.
wenzelm@6639
     1
(*  Title:      Pure/General/url.ML
wenzelm@6639
     2
    ID:         $Id$
wenzelm@6639
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6639
     4
wenzelm@6639
     5
Basic URLs.
wenzelm@6639
     6
*)
wenzelm@6639
     7
wenzelm@6639
     8
signature URL =
wenzelm@6639
     9
sig
wenzelm@6639
    10
  type T
wenzelm@6639
    11
  val file: Path.T -> T
wenzelm@6639
    12
  val http: string * Path.T -> T
wenzelm@6639
    13
  val ftp: string * Path.T -> T
wenzelm@6639
    14
  val append: T -> T -> T
wenzelm@6639
    15
  val pack: T -> string
wenzelm@6639
    16
  val unpack: string -> T
wenzelm@6639
    17
end;
wenzelm@6639
    18
wenzelm@6639
    19
structure Url: URL =
wenzelm@6639
    20
struct
wenzelm@6639
    21
wenzelm@6639
    22
wenzelm@6639
    23
(* type url *)
wenzelm@6639
    24
wenzelm@6639
    25
datatype scheme = File | Http of string | Ftp of string;
wenzelm@6639
    26
wenzelm@6639
    27
datatype T = Url of scheme * Path.T;
wenzelm@6639
    28
wenzelm@6639
    29
fun file p = Url (File, p);
wenzelm@6639
    30
fun http (h, p) = Url (Http h, p);
wenzelm@6639
    31
fun ftp (h, p) = Url (Ftp h, p);
wenzelm@6639
    32
wenzelm@6639
    33
wenzelm@6639
    34
(* append *)
wenzelm@6639
    35
wenzelm@6639
    36
fun append (Url (s, p)) (Url (File, p')) = Url (s, Path.append p p')
wenzelm@6639
    37
  | append _ url = url;
wenzelm@6639
    38
wenzelm@6639
    39
wenzelm@6639
    40
(* pack *)
wenzelm@6639
    41
wenzelm@6639
    42
fun pack_scheme File = ""
wenzelm@6639
    43
  | pack_scheme (Http host) = "http://" ^ host
wenzelm@6639
    44
  | pack_scheme (Ftp host) = "ftp://" ^ host;
wenzelm@6639
    45
wenzelm@6639
    46
fun pack (Url (s, p)) = pack_scheme s ^ (if Path.is_current p then "" else Path.pack p);
wenzelm@6639
    47
wenzelm@6639
    48
wenzelm@6639
    49
(* unpack *)
wenzelm@6639
    50
wenzelm@6639
    51
fun scan_lits [] x = ("", x)
wenzelm@6639
    52
  | scan_lits (c :: cs) x = (($$ c -- scan_lits cs) >> op ^) x;
wenzelm@6639
    53
wenzelm@6639
    54
val scan_literal = scan_lits o Symbol.explode;
wenzelm@6639
    55
wenzelm@6639
    56
val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
wenzelm@6639
    57
val scan_host = Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode;
wenzelm@6639
    58
wenzelm@6639
    59
val scan_url =
wenzelm@6639
    60
  scan_literal "http://" |-- scan_host -- scan_path >> http ||
wenzelm@6639
    61
  scan_literal "ftp://" |-- scan_host -- scan_path >> ftp ||
wenzelm@6639
    62
  Scan.unless (scan_literal "http:" || scan_literal "ftp:") scan_path >> file;
wenzelm@6639
    63
wenzelm@6639
    64
fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
wenzelm@6639
    65
wenzelm@6639
    66
wenzelm@6639
    67
end;