author | wenzelm |
Mon, 09 Dec 2013 12:16:52 +0100 | |
changeset 54702 | 3daeba5130f0 |
parent 29606 | fedb8be05f24 |
child 58854 | b979c781c2db |
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 |
RemoteFile of string * Path.T | |
|
12 |
Http of string * Path.T | |
|
13 |
Ftp of string * Path.T |
|
6639 | 14 |
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
|
15 |
val implode: T -> string |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
16 |
val explode: string -> T |
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
17 |
val pretty: T -> Pretty.T |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
18 |
val print: T -> string |
6639 | 19 |
end; |
20 |
||
21 |
structure Url: URL = |
|
22 |
struct |
|
23 |
||
24 |
(* type url *) |
|
25 |
||
14909 | 26 |
datatype T = |
27 |
File of Path.T | |
|
28 |
RemoteFile of string * Path.T | |
|
29 |
Http of string * Path.T | |
|
30 |
Ftp of string * Path.T; |
|
6639 | 31 |
|
32 |
||
33 |
(* append *) |
|
34 |
||
14909 | 35 |
fun append (File p) (File p') = File (Path.append p p') |
36 |
| append (RemoteFile (h, p)) (File p') = RemoteFile (h, Path.append p p') |
|
37 |
| append (Http (h, p)) (File p') = Http (h, Path.append p p') |
|
38 |
| append (Ftp (h, p)) (File p') = Ftp (h, Path.append p p') |
|
6639 | 39 |
| append _ url = url; |
40 |
||
41 |
||
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
42 |
(* implode *) |
6639 | 43 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
44 |
fun implode_path p = if Path.is_current p then "" else Path.implode p; |
6639 | 45 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
46 |
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
|
47 |
| 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
|
48 |
| 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
|
49 |
| implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p; |
6639 | 50 |
|
51 |
||
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
52 |
(* explode *) |
6639 | 53 |
|
14918 | 54 |
local |
55 |
||
16195 | 56 |
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
|
57 |
(Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --| |
14918 | 58 |
Scan.ahead ($$ "/" || Scan.one Symbol.is_eof); |
59 |
||
23784
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 = 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
|
61 |
val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode o implode o cons "/"); |
6639 | 62 |
|
63 |
val scan_url = |
|
14909 | 64 |
Scan.unless (Scan.this_string "file:" || |
65 |
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
|
66 |
Scan.this_string "file:///" |-- scan_path_root >> File || |
b62f7b493360
Fix file:/// and file://localhost/ to give absolute paths
aspinall
parents:
15174
diff
changeset
|
67 |
Scan.this_string "file://localhost/" |-- scan_path_root >> File || |
16195 | 68 |
Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile || |
21503 | 69 |
Scan.this_string "file:/" |-- scan_path_root >> File || |
16195 | 70 |
Scan.this_string "http://" |-- scan_host -- scan_path >> Http || |
71 |
Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp; |
|
14918 | 72 |
|
73 |
in |
|
6639 | 74 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
75 |
fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s); |
6639 | 76 |
|
77 |
end; |
|
14918 | 78 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
79 |
|
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
80 |
(* print *) |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
81 |
|
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
82 |
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
|
83 |
|
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
84 |
val print = Pretty.str_of o pretty; |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
85 |
|
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
29606
diff
changeset
|
86 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
87 |
(*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
|
88 |
val implode = implode_url; |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
89 |
val explode = explode_url; |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21515
diff
changeset
|
90 |
|
14918 | 91 |
end; |