common.anubis
3.83 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
*Project* The Anubis Project
*Title* Some common stuff for the web.
*Copyright* Copyright (c) Alain Prouté 2003.
*Author* Alain Prouté
*Public*
*Name* HTTP_header
*Description*
The type 'HTTP_header' describes HTTP headers, which are just pairs '(name,value)'.
public type HTTP_header:
http_header(String name,
String value).
*Name* Web_arg
*Description*
The type 'Web_arg' describes 'web arguments'. A web argument is either a pair
'(name,value)' (for example it may be 'web_arg("password","foobar")', if the client
clicks on the submit button of a form containing a password input field named
'password'), or an uploaded file. In this last case, it is a triplet containing the
name of the file upload input field, the value of this input field (name of the
uploaded file), and the name of the temporary file as saved by the server in its
'upload temporary directory'; see 'web/http_server.anubis' and the 'upload' Web_item in
'web/html.anubis').
public type Web_arg:
web_arg(String name,
String value),
upload (String name, // name of corresponding 'upload' Web_item
String value, // name of uploaded file
String temp_file_path). // temporary file path (relative to server directory)
*Name* Web_arg_value
*Description*
Of course, within the body of a 'web page' operation, you may want to recover the value
of a particular web argument. To that end, use the operation 'web_arg_value', which
takes 2 argument:
- the list of all web arguments (the operand of the web page operation),
- the name of the argument whose value is wanted.
This operation has the following return type:
public type Web_arg_value:
not_found,
found(String value).
*Name* Web_arg_value
*Description*
If the requested argument name is not found in the list, 'not_found' is
returned. Otherwise, the value returned by 'web_arg_value' has the form 'found(v)',
where 'v' is the value of the argument.
The operation 'web_arg_value' is defined below.
public define Web_arg_value
web_arg_value
(
List(Web_arg) l,
String name
) =
if l is
{
[ ] then not_found,
[h . t] then if h is
{
web_arg(n,v) then
if name=n
then found(v)
else web_arg_value(t,name),
upload(n,v,tfn) then
if name=n
then found(v)
else web_arg_value(t,name)
}
}.
*Ignore*
public define Maybe((String,String))
file_upload_value
(
List(Web_arg) l,
String name
) =
if l is
{
[ ] then failure,
[h . t] then if h is
{
web_arg(_,_) then file_upload_value(t,name),
upload(n,v,tfn) then
if n = name
then success((v,tfn))
else file_upload_value(t,name)
}
}.
public type Redirection:
redirect(String required_uri, // URI required by the client
String required_host, // value of 'Host' HTTP header sent by the client
String corresponding_uri). // URI which will be served to the client
Now, you may also want to recover web argument values which have been encoded (by
'web_arg_encode'). In this case, use the following:
read web/web_arg_encode.anubis
public define Maybe($T)
decode_web_arg_value
(
List(Web_arg) l,
String name
) =
if web_arg_value(l,name) is
{
not_found then failure,
found(v) then web_arg_decode(v)
}.