src/Pure/General/url.ML
author aspinall
Fri Nov 24 17:23:15 2006 +0100 (2006-11-24 ago)
changeset 21515 43d55165b282
parent 21503 c4ea7e8c3937
child 21858 05f57309170c
permissions -rw-r--r--
Comment: see RFC 2396 for relative URI syntax.
wenzelm@6639
     1
(*  Title:      Pure/General/url.ML
wenzelm@6639
     2
    ID:         $Id$
wenzelm@6639
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6639
     4
aspinall@21515
     5
Basic URLs, see RFC 1738 and RFC 2396.
wenzelm@6639
     6
*)
wenzelm@6639
     7
wenzelm@6639
     8
signature URL =
wenzelm@6639
     9
sig
wenzelm@14909
    10
  datatype T =
wenzelm@14909
    11
    File of Path.T |
wenzelm@14909
    12
    RemoteFile of string * Path.T |
wenzelm@14909
    13
    Http of string * Path.T |
wenzelm@14909
    14
    Ftp of string * Path.T
wenzelm@6639
    15
  val append: T -> T -> T
wenzelm@6639
    16
  val pack: T -> string
wenzelm@6639
    17
  val unpack: string -> T
wenzelm@6639
    18
end;
wenzelm@6639
    19
wenzelm@6639
    20
structure Url: URL =
wenzelm@6639
    21
struct
wenzelm@6639
    22
wenzelm@6639
    23
(* type url *)
wenzelm@6639
    24
wenzelm@14909
    25
datatype T =
wenzelm@14909
    26
  File of Path.T |
wenzelm@14909
    27
  RemoteFile of string * Path.T |
wenzelm@14909
    28
  Http of string * Path.T |
wenzelm@14909
    29
  Ftp of string * Path.T;
wenzelm@6639
    30
wenzelm@6639
    31
wenzelm@6639
    32
(* append *)
wenzelm@6639
    33
wenzelm@14909
    34
fun append (File p)            (File p') = File (Path.append p p')
wenzelm@14909
    35
  | append (RemoteFile (h, p)) (File p') = RemoteFile (h, Path.append p p')
wenzelm@14909
    36
  | append (Http (h, p))       (File p') = Http (h, Path.append p p')
wenzelm@14909
    37
  | append (Ftp (h, p))        (File p') = Ftp (h, Path.append p p')
wenzelm@6639
    38
  | append _ url = url;
wenzelm@6639
    39
wenzelm@6639
    40
wenzelm@6639
    41
(* pack *)
wenzelm@6639
    42
wenzelm@14909
    43
fun pack_path p = if Path.is_current p then "" else Path.pack p;
wenzelm@6639
    44
wenzelm@14909
    45
fun pack (File p) = pack_path p
wenzelm@14909
    46
  | pack (RemoteFile (h, p)) = "file://" ^ h ^ pack_path p
wenzelm@14909
    47
  | pack (Http (h, p)) = "http://" ^ h ^ pack_path p
wenzelm@14909
    48
  | pack (Ftp (h, p)) = "ftp://" ^ h ^ pack_path p;
wenzelm@6639
    49
wenzelm@6639
    50
wenzelm@6639
    51
(* unpack *)
wenzelm@6639
    52
wenzelm@14918
    53
local
wenzelm@14918
    54
wenzelm@16195
    55
val scan_host =
wenzelm@19305
    56
  (Scan.any1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
wenzelm@14918
    57
  Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
wenzelm@14918
    58
wenzelm@6639
    59
val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
wenzelm@16195
    60
val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o implode o cons "/");
wenzelm@6639
    61
wenzelm@6639
    62
val scan_url =
wenzelm@14909
    63
  Scan.unless (Scan.this_string "file:" ||
wenzelm@14909
    64
    Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
aspinall@15175
    65
  Scan.this_string "file:///" |-- scan_path_root >> File ||
aspinall@15175
    66
  Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
wenzelm@16195
    67
  Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile ||
aspinall@21503
    68
  Scan.this_string "file:/" |-- scan_path_root >> File ||
wenzelm@16195
    69
  Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
wenzelm@16195
    70
  Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
wenzelm@14918
    71
wenzelm@14918
    72
in
wenzelm@6639
    73
wenzelm@6639
    74
fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
wenzelm@6639
    75
wenzelm@6639
    76
end;
wenzelm@14918
    77
wenzelm@14918
    78
end;