From 7435b4f454396cfa8136e934aaa2aec9c91c58ac Mon Sep 17 00:00:00 2001 From: Colin Adams Date: Mon, 18 Mar 2013 14:45:04 +0000 Subject: [PATCH] refactored for WSF_ROUTED_SKELETON_SERVICE --- examples/restbucksCRUD/src/restbucks_server.e | 8 +- ...f_uri_template_helper_for_routed_service.e | 62 ++++ .../helpers/wsf_uri_template_routed_service.e | 44 +-- .../server/wsf/router/wsf_routed_service.e | 274 ++--------------- .../wsf/router/wsf_routed_skeleton_service.e | 279 ++++++++++++++++++ 5 files changed, 373 insertions(+), 294 deletions(-) create mode 100644 library/server/wsf/router/support/uri_template/helpers/wsf_uri_template_helper_for_routed_service.e create mode 100644 library/server/wsf/router/wsf_routed_skeleton_service.e diff --git a/examples/restbucksCRUD/src/restbucks_server.e b/examples/restbucksCRUD/src/restbucks_server.e index d9ebead2..653ce132 100644 --- a/examples/restbucksCRUD/src/restbucks_server.e +++ b/examples/restbucksCRUD/src/restbucks_server.e @@ -3,16 +3,16 @@ note date : "$Date$" revision : "$Revision$" -class - RESTBUCKS_SERVER +class RESTBUCKS_SERVER inherit - ANY - WSF_URI_TEMPLATE_ROUTED_SERVICE + WSF_ROUTED_SKELETON_SERVICE undefine requires_proxy end + + WSF_URI_TEMPLATE_HELPER_FOR_ROUTED_SERVICE WSF_HANDLER_HELPER diff --git a/library/server/wsf/router/support/uri_template/helpers/wsf_uri_template_helper_for_routed_service.e b/library/server/wsf/router/support/uri_template/helpers/wsf_uri_template_helper_for_routed_service.e new file mode 100644 index 00000000..e304aae0 --- /dev/null +++ b/library/server/wsf/router/support/uri_template/helpers/wsf_uri_template_helper_for_routed_service.e @@ -0,0 +1,62 @@ +note + + description: "Facilities inheritance to add URI template-base routing to a routed service" + + date: "$Date$" + revision: "$Revision$" + +deferred class WSF_URI_TEMPLATE_HELPER_FOR_ROUTED_SERVICE + +feature -- Access + + router: WSF_ROUTER + -- Router used to dispatch the request according to the WSF_REQUEST object + -- and associated request methods; + -- This should not be implemented by descendants. Instead, you gain an effective + -- version by also inheriting from WSF_ROUTED_SERVICE, or one of it's descendants. + deferred + ensure + router_not_void: Result /= Void + end + +feature -- Mapping helper: uri + + map_uri_template (a_tpl: STRING; h: WSF_URI_TEMPLATE_HANDLER) + -- Map `h' as handler for `a_tpl' + require + a_tpl_attached: a_tpl /= Void + h_attached: h /= Void + do + map_uri_template_with_request_methods (a_tpl, h, Void) + end + + map_uri_template_with_request_methods (a_tpl: READABLE_STRING_8; h: WSF_URI_TEMPLATE_HANDLER; rqst_methods: detachable WSF_REQUEST_METHODS) + -- Map `h' as handler for `a_tpl' for request methods `rqst_methods'. + require + a_tpl_attached: a_tpl /= Void + h_attached: h /= Void + do + router.map_with_request_methods (create {WSF_URI_TEMPLATE_MAPPING}.make (a_tpl, h), rqst_methods) + end + +feature -- Mapping helper: uri agent + + map_uri_template_agent (a_tpl: READABLE_STRING_8; proc: PROCEDURE [ANY, TUPLE [req: WSF_REQUEST; res: WSF_RESPONSE]]) + -- Map `proc' as handler for `a_tpl' + require + a_tpl_attached: a_tpl /= Void + proc_attached: proc /= Void + do + map_uri_template_agent_with_request_methods (a_tpl, proc, Void) + end + + map_uri_template_agent_with_request_methods (a_tpl: READABLE_STRING_8; proc: PROCEDURE [ANY, TUPLE [req: WSF_REQUEST; res: WSF_RESPONSE]]; rqst_methods: detachable WSF_REQUEST_METHODS) + -- Map `proc' as handler for `a_tpl' for request methods `rqst_methods'. + require + a_tpl_attached: a_tpl /= Void + proc_attached: proc /= Void + do + map_uri_template_with_request_methods (a_tpl, create {WSF_URI_TEMPLATE_AGENT_HANDLER}.make (proc), rqst_methods) + end + +end diff --git a/library/server/wsf/router/support/uri_template/helpers/wsf_uri_template_routed_service.e b/library/server/wsf/router/support/uri_template/helpers/wsf_uri_template_routed_service.e index 7dc8b5a6..51b27375 100644 --- a/library/server/wsf/router/support/uri_template/helpers/wsf_uri_template_routed_service.e +++ b/library/server/wsf/router/support/uri_template/helpers/wsf_uri_template_routed_service.e @@ -4,51 +4,13 @@ note date: "$Date$" revision: "$Revision$" -deferred class - WSF_URI_TEMPLATE_ROUTED_SERVICE +deferred class WSF_URI_TEMPLATE_ROUTED_SERVICE inherit + WSF_ROUTED_SERVICE -feature -- Mapping helper: uri - - map_uri_template (a_tpl: STRING; h: WSF_URI_TEMPLATE_HANDLER) - -- Map `h' as handler for `a_tpl' - require - a_tpl_attached: a_tpl /= Void - h_attached: h /= Void - do - map_uri_template_with_request_methods (a_tpl, h, Void) - end - - map_uri_template_with_request_methods (a_tpl: READABLE_STRING_8; h: WSF_URI_TEMPLATE_HANDLER; rqst_methods: detachable WSF_REQUEST_METHODS) - -- Map `h' as handler for `a_tpl' for request methods `rqst_methods'. - require - a_tpl_attached: a_tpl /= Void - h_attached: h /= Void - do - router.map_with_request_methods (create {WSF_URI_TEMPLATE_MAPPING}.make (a_tpl, h), rqst_methods) - end - -feature -- Mapping helper: uri agent - - map_uri_template_agent (a_tpl: READABLE_STRING_8; proc: PROCEDURE [ANY, TUPLE [req: WSF_REQUEST; res: WSF_RESPONSE]]) - -- Map `proc' as handler for `a_tpl' - require - a_tpl_attached: a_tpl /= Void - proc_attached: proc /= Void - do - map_uri_template_agent_with_request_methods (a_tpl, proc, Void) - end - - map_uri_template_agent_with_request_methods (a_tpl: READABLE_STRING_8; proc: PROCEDURE [ANY, TUPLE [req: WSF_REQUEST; res: WSF_RESPONSE]]; rqst_methods: detachable WSF_REQUEST_METHODS) - -- Map `proc' as handler for `a_tpl' for request methods `rqst_methods'. - require - a_tpl_attached: a_tpl /= Void - proc_attached: proc /= Void - do - map_uri_template_with_request_methods (a_tpl, create {WSF_URI_TEMPLATE_AGENT_HANDLER}.make (proc), rqst_methods) - end + WSF_URI_TEMPLATE_HELPER_FOR_ROUTED_SERVICE note copyright: "2011-2013, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others" diff --git a/library/server/wsf/router/wsf_routed_service.e b/library/server/wsf/router/wsf_routed_service.e index b4d16f23..22f7a0c1 100644 --- a/library/server/wsf/router/wsf_routed_service.e +++ b/library/server/wsf/router/wsf_routed_service.e @@ -4,40 +4,44 @@ note date: "$Date$" revision: "$Revision$" -deferred class WSF_ROUTED_SKELETON_SERVICE - -inherit - +deferred class WSF_ROUTED_SERVICE - redefine - execute + +feature -- Initialization + + initialize_router + -- Initialize router + do + create_router + setup_router end - WSF_SYSTEM_OPTIONS_ACCESS_POLICY + create_router + -- Create `router' + --| could be redefine to initialize with proper capacity + do + create router.make (10) + ensure + router_created: router /= Void + end - WSF_PROXY_USE_POLICY + setup_router + -- Setup `router' + require + router_created: router /= Void + deferred + end feature -- Execution execute (req: WSF_REQUEST; res: WSF_RESPONSE) - -- If the service is available, and request URI is not too long, dispatch the request + -- Dispatch the request -- and if handler is not found, execute the default procedure `execute_default'. require req_attached: req /= Void res_attached: res /= Void do - --| When we reach here, the request has already passed check for 400 (Bad request), - --| which is implemented in WSF_REQUEST.make_from_wgi (when it calls `analyze'). - if unavailable then - handle_unavailable (res) - elseif requires_proxy (req) then - handle_use_proxy (req, res) - elseif maximum_uri_length > 0 and then req.request_uri.count.to_natural_32 > maximum_uri_length then - handle_request_uri_too_long (res) - elseif req.is_request_method ({HTTP_REQUEST_METHODS}.method_options) and then - req.request_uri.same_string ("*") then - handle_server_options (req, res) - elseif attached router.dispatch_and_return_handler (req, res) as p then + if attached router.dispatch_and_return_handler (req, res) as p then -- executed else execute_default (req, res) @@ -58,9 +62,6 @@ feature -- Execution create msg.make_with_router (req, router) msg.set_documentation_included (True) res.send (msg) - ensure - response_status_is_set: res.status_is_set - message_sent: res.header_committed and res.message_committed end feature -- Access @@ -69,231 +70,6 @@ feature -- Access -- Router used to dispatch the request according to the WSF_REQUEST object -- and associated request methods -feature -- Measurement - - maximum_uri_length: NATURAL - -- Maximum length in characters (or zero for no limit) permitted - -- for {WSF_REQUEST}.request_uri - -feature -- Status report - - unavailable: BOOLEAN - -- Is service currently unavailable? - - unavailablity_message: detachable READABLE_STRING_8 - -- Message to be included as text of response body for {HTTP_STATUS_CODE}.service_unavailable - - unavailability_duration: NATURAL - -- Delta seconds for service unavailability (0 if not known) - - unavailable_until: detachable DATE_TIME - -- Time at which service becomes available again (if known) - -feature -- Status setting - - set_available - -- Set `unavailable' to `False'. - do - unavailable := False - unavailablity_message := Void - unavailable_until := Void - ensure - available: unavailable = False - unavailablity_message_detached: unavailablity_message = Void - unavailable_until_detached: unavailable_until = Void - end - - set_unavailable (a_message: READABLE_STRING_8; a_duration: NATURAL; a_until: detachable DATE_TIME) - -- Set `unavailable' to `True'. - require - a_message_attached: a_message /= Void - a_duration_xor_a_until: a_duration > 0 implies a_until = Void - do - unavailable := True - unavailablity_message := a_message - unavailability_duration := a_duration - ensure - unavailable: unavailable = True - unavailablity_message_aliased: unavailablity_message = a_message - unavailability_duration_set: unavailability_duration = a_duration - unavailable_until_aliased: unavailable_until = a_until - end - - set_maximum_uri_length (a_len: NATURAL) - -- Set `maximum_uri_length' to `a_len'. - -- Can pass zero to mean no restrictions. - do - maximum_uri_length := a_len - ensure - maximum_uri_length_set: maximum_uri_length = a_len - end - -feature {NONE} -- Implementation - - handle_unavailable (res: WSF_RESPONSE) - -- Write "Service unavailable" response to `res'. - require - unavailable: unavailable - res_attached: res /= Void - local - h: HTTP_HEADER - do - create h.make - h.put_content_type_text_plain - check attached unavailablity_message as m then - -- invariant plus precondition - h.put_content_length (m.count) - h.put_current_date - res.set_status_code ({HTTP_STATUS_CODE}.service_unavailable) - if unavailability_duration > 0 then - h.put_header_key_value ({HTTP_HEADER_NAMES}.header_retry_after, unavailability_duration.out) - elseif attached unavailable_until as u then - h.put_header_key_value ({HTTP_HEADER_NAMES}.header_retry_after, - h.date_to_rfc1123_http_date_format (u)) - end - res.put_header_text (h.string) - res.put_string (m) - end - ensure - response_status_is_set: res.status_is_set - status_is_service_unavailable: res.status_code = {HTTP_STATUS_CODE}.service_unavailable - body_sent: res.message_committed and then res.transfered_content_length > 0 - body_content_was_unavailablity_message: True -- doesn't seem to be any way to check - end - - handle_request_uri_too_long (res: WSF_RESPONSE) - -- Write "Request URI too long" response into `res'. - require - res_attached: res /= Void - local - h: HTTP_HEADER - m: READABLE_STRING_8 - do - create h.make - h.put_content_type_text_plain - h.put_current_date - m := "Maximum permitted length for request URI is " + maximum_uri_length.out + " characters" - h.put_content_length (m.count) - res.set_status_code ({HTTP_STATUS_CODE}.request_uri_too_long) - res.put_header_text (h.string) - res.put_string (m) - ensure - response_status_is_set: res.status_is_set - status_is_request_uri_too_long: res.status_code = {HTTP_STATUS_CODE}.request_uri_too_long - body_sent: res.message_committed and then res.transfered_content_length > 0 - end - - frozen handle_server_options (req: WSF_REQUEST; res: WSF_RESPONSE) - -- Write response to OPTIONS * into `res'. - require - req_attached: req /= Void - res_attached: res /= Void - method_is_options: req.is_request_method ({HTTP_REQUEST_METHODS}.method_options) - server_options_requested: req.request_uri.same_string ("*") - do - --| First check if forbidden. - --| (N.B. authentication requires an absoluteURI (RFC3617 page 3), and so cannot be used for OPTIONS *. - --| Otherwise construct an Allow response automatically from the router. - if is_system_options_forbidden (req) then - handle_system_options_forbidden (req, res) - else - handle_system_options (req, res) - end - ensure - response_status_is_set: res.status_is_set - valid_response_code: res.status_code = {HTTP_STATUS_CODE}.forbidden or - res.status_code = {HTTP_STATUS_CODE}.not_found or res.status_code = {HTTP_STATUS_CODE}.ok - header_sent: res.header_committed and res.message_committed - end - - frozen handle_system_options_forbidden (req: WSF_REQUEST; res: WSF_RESPONSE) - -- Write a 403 Forbidden or a 404 Not found response into `res'. - require - req_attached: req /= Void - res_attached: res /= Void - method_is_options: req.is_request_method ({HTTP_REQUEST_METHODS}.method_options) - server_options_requested: req.request_uri.same_string ("*") - local - m: detachable READABLE_STRING_8 - h: HTTP_HEADER - do - m := system_options_forbidden_text (req) - if attached {READABLE_STRING_8} m as l_msg then - create h.make - h.put_content_type_text_plain - h.put_current_date - h.put_content_length (l_msg.count) - res.set_status_code ({HTTP_STATUS_CODE}.forbidden) - res.put_header_text (h.string) - res.put_string (l_msg) - else - create h.make - h.put_content_type_text_plain - h.put_current_date - h.put_content_length (0) - res.set_status_code ({HTTP_STATUS_CODE}.not_found) - res.put_header_text (h.string) - end - ensure - response_status_is_set: res.status_is_set - valid_response_code: res.status_code = {HTTP_STATUS_CODE}.forbidden or - res.status_code = {HTTP_STATUS_CODE}.not_found - header_sent: res.header_committed - message_sent: res.message_committed - end - - handle_system_options (req: WSF_REQUEST; res: WSF_RESPONSE) - -- Write response to OPTIONS * into `res'. - -- This may be redefined by the user, but normally this will not be necessary. - require - req_attached: req /= Void - res_attached: res /= Void - method_is_options: req.is_request_method ({HTTP_REQUEST_METHODS}.method_options) - server_options_requested: req.request_uri.same_string ("*") - local - h: HTTP_HEADER - do - create h.make - h.put_content_type_text_plain - h.put_current_date - h.put_allow (router.all_allowed_methods) - h.put_content_length (0) - res.set_status_code ({HTTP_STATUS_CODE}.ok) - res.put_header_text (h.string) - ensure - response_status_is_set: res.status_is_set - response_code_ok: res.status_code = {HTTP_STATUS_CODE}.ok - header_sent: res.header_committed and res.message_committed - empty_body: res.transfered_content_length = 0 - end - - frozen handle_use_proxy (req: WSF_REQUEST; res: WSF_RESPONSE) - -- Write response to OPTIONS * into `res'. - require - res_attached: res /= Void - req_attached: req /= Void - proxy_required: requires_proxy (req) - local - h: HTTP_HEADER - do - create h.make - h.put_content_type_text_plain - h.put_current_date - h.put_location (proxy_server (req)) - h.put_content_length (0) - res.set_status_code ({HTTP_STATUS_CODE}.use_proxy) - ensure - response_status_is_set: res.status_is_set - response_code_use_proxy: res.status_code = {HTTP_STATUS_CODE}.use_proxy - header_sent: res.header_committed and res.message_committed - end - -invariant - - unavailability_message_attached: unavailable implies attached unavailablity_message as m and then - m.count > 0 - unavailability_duration_xor_unavailable_until: unavailability_duration > 0 implies unavailable_until = Void - ;note copyright: "2011-2013, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" diff --git a/library/server/wsf/router/wsf_routed_skeleton_service.e b/library/server/wsf/router/wsf_routed_skeleton_service.e new file mode 100644 index 00000000..8f50331f --- /dev/null +++ b/library/server/wsf/router/wsf_routed_skeleton_service.e @@ -0,0 +1,279 @@ +note + description: "Summary description for {WSF_ROUTED_SERVICE}." + author: "" + date: "$Date$" + revision: "$Revision$" + +deferred class WSF_ROUTED_SKELETON_SERVICE + +inherit + + WSF_ROUTED_SERVICE + redefine + execute + end + + WSF_SYSTEM_OPTIONS_ACCESS_POLICY + + WSF_PROXY_USE_POLICY + +feature -- Execution + + execute (req: WSF_REQUEST; res: WSF_RESPONSE) + -- If the service is available, and request URI is not too long, dispatch the request + -- and if handler is not found, execute the default procedure `execute_default'. + do + --| When we reach here, the request has already passed check for 400 (Bad request), + --| which is implemented in WSF_REQUEST.make_from_wgi (when it calls `analyze'). + if unavailable then + handle_unavailable (res) + elseif requires_proxy (req) then + handle_use_proxy (req, res) + elseif maximum_uri_length > 0 and then req.request_uri.count.to_natural_32 > maximum_uri_length then + handle_request_uri_too_long (res) + elseif req.is_request_method ({HTTP_REQUEST_METHODS}.method_options) and then + req.request_uri.same_string ("*") then + handle_server_options (req, res) + elseif attached router.dispatch_and_return_handler (req, res) as p then + -- executed + else + execute_default (req, res) + end + end + +feature -- Measurement + + maximum_uri_length: NATURAL + -- Maximum length in characters (or zero for no limit) permitted + -- for {WSF_REQUEST}.request_uri + +feature -- Status report + + unavailable: BOOLEAN + -- Is service currently unavailable? + + unavailablity_message: detachable READABLE_STRING_8 + -- Message to be included as text of response body for {HTTP_STATUS_CODE}.service_unavailable + + unavailability_duration: NATURAL + -- Delta seconds for service unavailability (0 if not known) + + unavailable_until: detachable DATE_TIME + -- Time at which service becomes available again (if known) + +feature -- Status setting + + set_available + -- Set `unavailable' to `False'. + do + unavailable := False + unavailablity_message := Void + unavailable_until := Void + ensure + available: unavailable = False + unavailablity_message_detached: unavailablity_message = Void + unavailable_until_detached: unavailable_until = Void + end + + set_unavailable (a_message: READABLE_STRING_8; a_duration: NATURAL; a_until: detachable DATE_TIME) + -- Set `unavailable' to `True'. + require + a_message_attached: a_message /= Void + a_duration_xor_a_until: a_duration > 0 implies a_until = Void + do + unavailable := True + unavailablity_message := a_message + unavailability_duration := a_duration + ensure + unavailable: unavailable = True + unavailablity_message_aliased: unavailablity_message = a_message + unavailability_duration_set: unavailability_duration = a_duration + unavailable_until_aliased: unavailable_until = a_until + end + + set_maximum_uri_length (a_len: NATURAL) + -- Set `maximum_uri_length' to `a_len'. + -- Can pass zero to mean no restrictions. + do + maximum_uri_length := a_len + ensure + maximum_uri_length_set: maximum_uri_length = a_len + end + +feature {NONE} -- Implementation + + handle_unavailable (res: WSF_RESPONSE) + -- Write "Service unavailable" response to `res'. + require + unavailable: unavailable + res_attached: res /= Void + local + h: HTTP_HEADER + do + create h.make + h.put_content_type_text_plain + check attached unavailablity_message as m then + -- invariant plus precondition + h.put_content_length (m.count) + h.put_current_date + res.set_status_code ({HTTP_STATUS_CODE}.service_unavailable) + if unavailability_duration > 0 then + h.put_header_key_value ({HTTP_HEADER_NAMES}.header_retry_after, unavailability_duration.out) + elseif attached unavailable_until as u then + h.put_header_key_value ({HTTP_HEADER_NAMES}.header_retry_after, + h.date_to_rfc1123_http_date_format (u)) + end + res.put_header_text (h.string) + res.put_string (m) + end + ensure + response_status_is_set: res.status_is_set + status_is_service_unavailable: res.status_code = {HTTP_STATUS_CODE}.service_unavailable + body_sent: res.message_committed and then res.transfered_content_length > 0 + body_content_was_unavailablity_message: True -- doesn't seem to be any way to check + end + + handle_request_uri_too_long (res: WSF_RESPONSE) + -- Write "Request URI too long" response into `res'. + require + res_attached: res /= Void + local + h: HTTP_HEADER + m: READABLE_STRING_8 + do + create h.make + h.put_content_type_text_plain + h.put_current_date + m := "Maximum permitted length for request URI is " + maximum_uri_length.out + " characters" + h.put_content_length (m.count) + res.set_status_code ({HTTP_STATUS_CODE}.request_uri_too_long) + res.put_header_text (h.string) + res.put_string (m) + ensure + response_status_is_set: res.status_is_set + status_is_request_uri_too_long: res.status_code = {HTTP_STATUS_CODE}.request_uri_too_long + body_sent: res.message_committed and then res.transfered_content_length > 0 + end + + frozen handle_server_options (req: WSF_REQUEST; res: WSF_RESPONSE) + -- Write response to OPTIONS * into `res'. + require + req_attached: req /= Void + res_attached: res /= Void + method_is_options: req.is_request_method ({HTTP_REQUEST_METHODS}.method_options) + server_options_requested: req.request_uri.same_string ("*") + do + --| First check if forbidden. + --| (N.B. authentication requires an absoluteURI (RFC3617 page 3), and so cannot be used for OPTIONS *. + --| Otherwise construct an Allow response automatically from the router. + if is_system_options_forbidden (req) then + handle_system_options_forbidden (req, res) + else + handle_system_options (req, res) + end + ensure + response_status_is_set: res.status_is_set + valid_response_code: res.status_code = {HTTP_STATUS_CODE}.forbidden or + res.status_code = {HTTP_STATUS_CODE}.not_found or res.status_code = {HTTP_STATUS_CODE}.ok + header_sent: res.header_committed and res.message_committed + end + + frozen handle_system_options_forbidden (req: WSF_REQUEST; res: WSF_RESPONSE) + -- Write a 403 Forbidden or a 404 Not found response into `res'. + require + req_attached: req /= Void + res_attached: res /= Void + method_is_options: req.is_request_method ({HTTP_REQUEST_METHODS}.method_options) + server_options_requested: req.request_uri.same_string ("*") + local + m: detachable READABLE_STRING_8 + h: HTTP_HEADER + do + m := system_options_forbidden_text (req) + if attached {READABLE_STRING_8} m as l_msg then + create h.make + h.put_content_type_text_plain + h.put_current_date + h.put_content_length (l_msg.count) + res.set_status_code ({HTTP_STATUS_CODE}.forbidden) + res.put_header_text (h.string) + res.put_string (l_msg) + else + create h.make + h.put_content_type_text_plain + h.put_current_date + h.put_content_length (0) + res.set_status_code ({HTTP_STATUS_CODE}.not_found) + res.put_header_text (h.string) + end + ensure + response_status_is_set: res.status_is_set + valid_response_code: res.status_code = {HTTP_STATUS_CODE}.forbidden or + res.status_code = {HTTP_STATUS_CODE}.not_found + header_sent: res.header_committed + message_sent: res.message_committed + end + + handle_system_options (req: WSF_REQUEST; res: WSF_RESPONSE) + -- Write response to OPTIONS * into `res'. + -- This may be redefined by the user, but normally this will not be necessary. + require + req_attached: req /= Void + res_attached: res /= Void + method_is_options: req.is_request_method ({HTTP_REQUEST_METHODS}.method_options) + server_options_requested: req.request_uri.same_string ("*") + local + h: HTTP_HEADER + do + create h.make + h.put_content_type_text_plain + h.put_current_date + h.put_allow (router.all_allowed_methods) + h.put_content_length (0) + res.set_status_code ({HTTP_STATUS_CODE}.ok) + res.put_header_text (h.string) + ensure + response_status_is_set: res.status_is_set + response_code_ok: res.status_code = {HTTP_STATUS_CODE}.ok + header_sent: res.header_committed and res.message_committed + empty_body: res.transfered_content_length = 0 + end + + frozen handle_use_proxy (req: WSF_REQUEST; res: WSF_RESPONSE) + -- Write response to OPTIONS * into `res'. + require + res_attached: res /= Void + req_attached: req /= Void + proxy_required: requires_proxy (req) + local + h: HTTP_HEADER + do + create h.make + h.put_content_type_text_plain + h.put_current_date + h.put_location (proxy_server (req)) + h.put_content_length (0) + res.set_status_code ({HTTP_STATUS_CODE}.use_proxy) + ensure + response_status_is_set: res.status_is_set + response_code_use_proxy: res.status_code = {HTTP_STATUS_CODE}.use_proxy + header_sent: res.header_committed and res.message_committed + end + +invariant + + unavailability_message_attached: unavailable implies attached unavailablity_message as m and then + m.count > 0 + unavailability_duration_xor_unavailable_until: unavailability_duration > 0 implies unavailable_until = Void + +;note + copyright: "2011-2013, Jocelyn Fiat, Javier Velilla, Olivier Ligot, Eiffel Software and others" + license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" + source: "[ + Eiffel Software + 5949 Hollister Ave., Goleta, CA 93117 USA + Telephone 805-685-1006, Fax 805-685-6869 + Website http://www.eiffel.com + Customer support http://support.eiffel.com + ]" +end