src/Pure/General/url.ML
author wenzelm
Wed Jan 21 23:21:44 2009 +0100 (2009-01-21 ago)
changeset 29606 fedb8be05f24
parent 23784 75e6b9dd5336
child 54702 3daeba5130f0
permissions -rw-r--r--
removed Ids;
wenzelm@6639
     1
(*  Title:      Pure/General/url.ML
wenzelm@6639
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6639
     3
aspinall@21515
     4
Basic URLs, see RFC 1738 and RFC 2396.
wenzelm@6639
     5
*)
wenzelm@6639
     6
wenzelm@6639
     7
signature URL =
wenzelm@6639
     8
sig
wenzelm@14909
     9
  datatype T =
wenzelm@14909
    10
    File of Path.T |
wenzelm@14909
    11
    RemoteFile of string * Path.T |
wenzelm@14909
    12
    Http of string * Path.T |
wenzelm@14909
    13
    Ftp of string * Path.T
wenzelm@6639
    14
  val append: T -> T -> T
wenzelm@21858
    15
  val implode: T -> string
wenzelm@21858
    16
  val explode: 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
(* type url *)
wenzelm@6639
    23
wenzelm@14909
    24
datatype T =
wenzelm@14909
    25
  File of Path.T |
wenzelm@14909
    26
  RemoteFile of string * Path.T |
wenzelm@14909
    27
  Http of string * Path.T |
wenzelm@14909
    28
  Ftp of string * Path.T;
wenzelm@6639
    29
wenzelm@6639
    30
wenzelm@6639
    31
(* append *)
wenzelm@6639
    32
wenzelm@14909
    33
fun append (File p)            (File p') = File (Path.append p p')
wenzelm@14909
    34
  | append (RemoteFile (h, p)) (File p') = RemoteFile (h, Path.append p p')
wenzelm@14909
    35
  | append (Http (h, p))       (File p') = Http (h, Path.append p p')
wenzelm@14909
    36
  | append (Ftp (h, p))        (File p') = Ftp (h, Path.append p p')
wenzelm@6639
    37
  | append _ url = url;
wenzelm@6639
    38
wenzelm@6639
    39
wenzelm@21858
    40
(* implode *)
wenzelm@6639
    41
wenzelm@21858
    42
fun implode_path p = if Path.is_current p then "" else Path.implode p;
wenzelm@6639
    43
wenzelm@21858
    44
fun implode_url (File p) = implode_path p
wenzelm@21858
    45
  | implode_url (RemoteFile (h, p)) = "file://" ^ h ^ implode_path p
wenzelm@21858
    46
  | implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
wenzelm@21858
    47
  | implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
wenzelm@6639
    48
wenzelm@6639
    49
wenzelm@21858
    50
(* explode *)
wenzelm@6639
    51
wenzelm@14918
    52
local
wenzelm@14918
    53
wenzelm@16195
    54
val scan_host =
wenzelm@23784
    55
  (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --|
wenzelm@14918
    56
  Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
wenzelm@14918
    57
wenzelm@23784
    58
val scan_path = Scan.many Symbol.is_regular >> (Path.explode o implode);
wenzelm@23784
    59
val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode o implode o cons "/");
wenzelm@6639
    60
wenzelm@6639
    61
val scan_url =
wenzelm@14909
    62
  Scan.unless (Scan.this_string "file:" ||
wenzelm@14909
    63
    Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
aspinall@15175
    64
  Scan.this_string "file:///" |-- scan_path_root >> File ||
aspinall@15175
    65
  Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
wenzelm@16195
    66
  Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile ||
aspinall@21503
    67
  Scan.this_string "file:/" |-- scan_path_root >> File ||
wenzelm@16195
    68
  Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
wenzelm@16195
    69
  Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
wenzelm@14918
    70
wenzelm@14918
    71
in
wenzelm@6639
    72
wenzelm@21858
    73
fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
wenzelm@6639
    74
wenzelm@6639
    75
end;
wenzelm@14918
    76
wenzelm@21858
    77
wenzelm@21858
    78
(*final declarations of this structure!*)
wenzelm@21858
    79
val implode = implode_url;
wenzelm@21858
    80
val explode = explode_url;
wenzelm@21858
    81
wenzelm@14918
    82
end;