author | wenzelm |
Sun, 30 Apr 2017 09:23:03 +0200 | |
changeset 65641 | 3b0110e25745 |
parent 64776 | 3f20c63f71be |
child 68226 | 5ce62512de35 |
permissions | -rw-r--r-- |
6639 | 1 |
(* Title: Pure/General/url.ML |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
||
21515 | 4 |
Basic URLs, see RFC 1738 and RFC 2396. |
6639 | 5 |
*) |
6 |
||
7 |
signature URL = |
|
8 |
sig |
|
14909 | 9 |
datatype T = |
10 |
File of Path.T | |
|
11 |
Http of string * Path.T | |
|
12 |
Ftp of string * Path.T |
|
6639 | 13 |
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
|
14 |
val implode: T -> string |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
15 |
val explode: string -> T |
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
16 |
val pretty: T -> Pretty.T |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
17 |
val print: T -> string |
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 |
Http of string * Path.T | |
|
28 |
Ftp of string * Path.T; |
|
6639 | 29 |
|
30 |
||
31 |
(* append *) |
|
32 |
||
64776 | 33 |
fun append (File p) (File p') = File (Path.append p p') |
34 |
| append (Http (h, p)) (File p') = Http (h, Path.append p p') |
|
35 |
| append (Ftp (h, p)) (File p') = Ftp (h, Path.append p p') |
|
6639 | 36 |
| append _ url = url; |
37 |
||
38 |
||
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
39 |
(* implode *) |
6639 | 40 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
41 |
fun implode_path p = if Path.is_current p then "" else Path.implode p; |
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_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
|
44 |
| 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
|
45 |
| implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p; |
6639 | 46 |
|
47 |
||
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
48 |
(* explode *) |
6639 | 49 |
|
14918 | 50 |
local |
51 |
||
16195 | 52 |
val scan_host = |
58854 | 53 |
(Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --| |
14918 | 54 |
Scan.ahead ($$ "/" || Scan.one Symbol.is_eof); |
55 |
||
58854 | 56 |
val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode); |
57 |
val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/"); |
|
6639 | 58 |
|
59 |
val scan_url = |
|
14909 | 60 |
Scan.unless (Scan.this_string "file:" || |
61 |
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
|
62 |
Scan.this_string "file:///" |-- scan_path_root >> File || |
b62f7b493360
Fix file:/// and file://localhost/ to give absolute paths
aspinall
parents:
15174
diff
changeset
|
63 |
Scan.this_string "file://localhost/" |-- scan_path_root >> File || |
64776 | 64 |
Scan.this_string "file://" |-- scan_host -- scan_path |
65 |
>> (fn (h, p) => File (Path.append (Path.named_root h) p)) || |
|
21503 | 66 |
Scan.this_string "file:/" |-- scan_path_root >> File || |
16195 | 67 |
Scan.this_string "http://" |-- scan_host -- scan_path >> Http || |
68 |
Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp; |
|
14918 | 69 |
|
70 |
in |
|
6639 | 71 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
72 |
fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s); |
6639 | 73 |
|
74 |
end; |
|
14918 | 75 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
76 |
|
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
77 |
(* print *) |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
78 |
|
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
79 |
val pretty = Pretty.mark_str o `Markup.url o implode_url; |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
80 |
|
61877
276ad4354069
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents:
58854
diff
changeset
|
81 |
val print = Pretty.unformatted_string_of o pretty; |
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
82 |
|
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
83 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
84 |
(*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
|
85 |
val implode = implode_url; |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
86 |
val explode = explode_url; |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
87 |
|
14918 | 88 |
end; |