author | haftmann |
Tue, 23 Sep 2008 18:11:44 +0200 | |
changeset 28337 | 93964076e7b8 |
parent 23784 | 75e6b9dd5336 |
child 29606 | fedb8be05f24 |
permissions | -rw-r--r-- |
6639 | 1 |
(* Title: Pure/General/url.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
21515 | 5 |
Basic URLs, see RFC 1738 and RFC 2396. |
6639 | 6 |
*) |
7 |
||
8 |
signature URL = |
|
9 |
sig |
|
14909 | 10 |
datatype T = |
11 |
File of Path.T | |
|
12 |
RemoteFile of string * Path.T | |
|
13 |
Http of string * Path.T | |
|
14 |
Ftp of string * Path.T |
|
6639 | 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 | 18 |
end; |
19 |
||
20 |
structure Url: URL = |
|
21 |
struct |
|
22 |
||
23 |
(* type url *) |
|
24 |
||
14909 | 25 |
datatype T = |
26 |
File of Path.T | |
|
27 |
RemoteFile of string * Path.T | |
|
28 |
Http of string * Path.T | |
|
29 |
Ftp of string * Path.T; |
|
6639 | 30 |
|
31 |
||
32 |
(* append *) |
|
33 |
||
14909 | 34 |
fun append (File p) (File p') = File (Path.append p p') |
35 |
| append (RemoteFile (h, p)) (File p') = RemoteFile (h, Path.append p p') |
|
36 |
| append (Http (h, p)) (File p') = Http (h, Path.append p p') |
|
37 |
| append (Ftp (h, p)) (File p') = Ftp (h, Path.append p p') |
|
6639 | 38 |
| append _ url = url; |
39 |
||
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 | 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 | 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 | 49 |
|
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 | 52 |
|
14918 | 53 |
local |
54 |
||
16195 | 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 | 57 |
Scan.ahead ($$ "/" || Scan.one Symbol.is_eof); |
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 | 61 |
|
62 |
val scan_url = |
|
14909 | 63 |
Scan.unless (Scan.this_string "file:" || |
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 | 67 |
Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile || |
21503 | 68 |
Scan.this_string "file:/" |-- scan_path_root >> File || |
16195 | 69 |
Scan.this_string "http://" |-- scan_host -- scan_path >> Http || |
70 |
Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp; |
|
14918 | 71 |
|
72 |
in |
|
6639 | 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 | 75 |
|
76 |
end; |
|
14918 | 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 | 83 |
end; |