src/Pure/General/url.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23784 75e6b9dd5336
child 29606 fedb8be05f24
permissions -rw-r--r--
tuned signature;
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@21858
    16
  val implode: T -> string
wenzelm@21858
    17
  val explode: 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@21858
    41
(* implode *)
wenzelm@6639
    42
wenzelm@21858
    43
fun implode_path p = if Path.is_current p then "" else Path.implode p;
wenzelm@6639
    44
wenzelm@21858
    45
fun implode_url (File p) = implode_path p
wenzelm@21858
    46
  | implode_url (RemoteFile (h, p)) = "file://" ^ h ^ implode_path p
wenzelm@21858
    47
  | implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
wenzelm@21858
    48
  | implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
wenzelm@6639
    49
wenzelm@6639
    50
wenzelm@21858
    51
(* explode *)
wenzelm@6639
    52
wenzelm@14918
    53
local
wenzelm@14918
    54
wenzelm@16195
    55
val scan_host =
wenzelm@23784
    56
  (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --|
wenzelm@14918
    57
  Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
wenzelm@14918
    58
wenzelm@23784
    59
val scan_path = Scan.many Symbol.is_regular >> (Path.explode o implode);
wenzelm@23784
    60
val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode 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@21858
    74
fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
wenzelm@6639
    75
wenzelm@6639
    76
end;
wenzelm@14918
    77
wenzelm@21858
    78
wenzelm@21858
    79
(*final declarations of this structure!*)
wenzelm@21858
    80
val implode = implode_url;
wenzelm@21858
    81
val explode = explode_url;
wenzelm@21858
    82
wenzelm@14918
    83
end;