src/Pure/General/url.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 23784 75e6b9dd5336
child 29606 fedb8be05f24
permissions -rw-r--r--
filtering out some package theorems
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
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
     4
21515
43d55165b282 Comment: see RFC 2396 for relative URI syntax.
aspinall
parents: 21503
diff changeset
     5
Basic URLs, see RFC 1738 and RFC 2396.
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
     6
*)
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
     7
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
     8
signature URL =
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
     9
sig
14909
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    10
  datatype T =
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    11
    File of Path.T |
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    12
    RemoteFile of string * Path.T |
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    13
    Http of string * Path.T |
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    14
    Ftp of string * Path.T
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    15
  val append: T -> T -> T
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    16
  val implode: T -> string
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    17
  val explode: string -> T
6639
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
(* type url *)
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    24
14909
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    25
datatype T =
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    26
  File of Path.T |
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    27
  RemoteFile of string * Path.T |
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    28
  Http of string * Path.T |
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    29
  Ftp of string * Path.T;
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    30
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    31
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    32
(* append *)
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    33
14909
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    34
fun append (File p)            (File p') = File (Path.append p p')
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    35
  | append (RemoteFile (h, p)) (File p') = RemoteFile (h, Path.append p p')
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    36
  | append (Http (h, p))       (File p') = Http (h, Path.append p p')
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    37
  | append (Ftp (h, p))        (File p') = Ftp (h, Path.append p p')
6639
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
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    41
(* implode *)
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    42
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    43
fun implode_path p = if Path.is_current p then "" else Path.implode p;
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    44
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    45
fun implode_url (File p) = implode_path p
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    46
  | implode_url (RemoteFile (h, p)) = "file://" ^ h ^ implode_path p
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    47
  | implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    48
  | implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    49
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    50
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    51
(* explode *)
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    52
14918
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    53
local
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    54
16195
wenzelm
parents: 15627
diff changeset
    55
val scan_host =
23784
75e6b9dd5336 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 21858
diff changeset
    56
  (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --|
14918
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    57
  Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    58
23784
75e6b9dd5336 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 21858
diff changeset
    59
val scan_path = Scan.many Symbol.is_regular >> (Path.explode o implode);
75e6b9dd5336 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 21858
diff changeset
    60
val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode o implode o cons "/");
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    61
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    62
val scan_url =
14909
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    63
  Scan.unless (Scan.this_string "file:" ||
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    64
    Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
15175
b62f7b493360 Fix file:/// and file://localhost/ to give absolute paths
aspinall
parents: 15174
diff changeset
    65
  Scan.this_string "file:///" |-- scan_path_root >> File ||
b62f7b493360 Fix file:/// and file://localhost/ to give absolute paths
aspinall
parents: 15174
diff changeset
    66
  Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
16195
wenzelm
parents: 15627
diff changeset
    67
  Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile ||
21503
c4ea7e8c3937 Accept URLs of form file:/home... also.
aspinall
parents: 19305
diff changeset
    68
  Scan.this_string "file:/" |-- scan_path_root >> File ||
16195
wenzelm
parents: 15627
diff changeset
    69
  Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
wenzelm
parents: 15627
diff changeset
    70
  Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
14918
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    71
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    72
in
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    73
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    74
fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    75
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    76
end;
14918
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    77
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    78
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    79
(*final declarations of this structure!*)
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    80
val implode = implode_url;
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    81
val explode = explode_url;
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21515
diff changeset
    82
14918
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    83
end;