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