mirrors/EWF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Actioned Jocelyns comments re. a_req and a_res

Browse Source
This commit is contained in:
Colin Adams
2012-12-11 19:26:06 +00:00
parent 365da7e30a
commit eafb04719d
3 changed files with 34 additions and 34 deletions
Download Patch File Download Diff File Expand all files Collapse all files

22
library/server/wsf/extension/wsf_method_handler.e
View File

@@ -10,16 +10,16 @@ deferred class WSF_METHOD_HANDLER
feature -- Method
do_method (a_req: WSF_REQUEST; a_res: WSF_RESPONSE)
-- Respond to `a_req' using `a_res'.
do_method (req: WSF_REQUEST; res: WSF_RESPONSE)
-- Respond to `req' using `res'.
require
a_req_not_void: a_req /= Void
a_res_not_void: a_res /= Void
req_not_void: req /= Void
res_not_void: res /= Void
deferred
ensure
valid_response_for_http_1_0: is_1_0 (a_req.server_protocol) implies
valid_response_for_http_1_0 (a_res.status_code)
empty_body_for_no_content_response: is_no_content_response (a_res.status_code) implies is_empty_content (a_res)
valid_response_for_http_1_0: is_1_0 (req.server_protocol) implies
valid_response_for_http_1_0 (res.status_code)
empty_body_for_no_content_response: is_no_content_response (res.status_code) implies is_empty_content (res)
end
feature -- Contract support
@@ -60,12 +60,12 @@ feature -- Contract support
end
end
is_empty_content (a_res: WSF_RESPONSE): BOOLEAN
-- Does `a_res' not contain an entity?
is_empty_content (res: WSF_RESPONSE): BOOLEAN
-- Does `res' not contain an entity?
require
a_res_not_void: a_res /= Void
res_not_void: res /= Void
do
Result := a_res.transfered_content_length = 0 -- Is that the right measure?
Result := res.transfered_content_length = 0 -- Is that the right measure?
end
end

24
library/server/wsf/extension/wsf_method_handlers.e
View File

@@ -49,28 +49,28 @@ inherit
feature -- Method
do_head (a_req: WSF_REQUEST; a_res: WSF_RESPONSE)
-- Respond to `a_req' using `a_res'.
do_head (req: WSF_REQUEST; res: WSF_RESPONSE)
-- Respond to `req' using `res'.
deferred
ensure then
empty_body: is_empty_content (a_res)
empty_body: is_empty_content (res)
end
do_post (a_req: WSF_REQUEST; a_res: WSF_RESPONSE)
-- Respond to `a_req' using `a_res'.
do_post (req: WSF_REQUEST; res: WSF_RESPONSE)
-- Respond to `req' using `res'.
deferred
ensure then
non_empty_body: a_res.status_code = {HTTP_STATUS_CODE}.created implies
not is_empty_content (a_res)
location_header: a_res.status_code = {HTTP_STATUS_CODE}.created implies True -- WSF_RESPONSE needs enhancing
non_empty_body: res.status_code = {HTTP_STATUS_CODE}.created implies
not is_empty_content (res)
location_header: res.status_code = {HTTP_STATUS_CODE}.created implies True -- WSF_RESPONSE needs enhancing
end
do_trace (a_req: WSF_REQUEST; a_res: WSF_RESPONSE)
-- Respond to `a_req' using `a_res'.
do_trace (req: WSF_REQUEST; res: WSF_RESPONSE)
-- Respond to `req' using `res'.
deferred
ensure then
non_empty_body: a_res.status_code = {HTTP_STATUS_CODE}.ok implies
not is_empty_content (a_res)
non_empty_body: res.status_code = {HTTP_STATUS_CODE}.ok implies
not is_empty_content (res)
end
end