diff --git a/library/server/wsf/router/documentation/wsf_router_self_documentation_handler.e b/library/server/wsf/router/documentation/wsf_router_self_documentation_handler.e index b0fbb6da..8ab6c2ab 100644 --- a/library/server/wsf/router/documentation/wsf_router_self_documentation_handler.e +++ b/library/server/wsf/router/documentation/wsf_router_self_documentation_handler.e @@ -26,14 +26,27 @@ create feature {NONE} -- Initialization make (a_router: WSF_ROUTER) + -- Initialize `router'. + require + a_router_attached: a_router /= Void do router := a_router + ensure + router_aliased: router = a_router + not_hidden: not is_hidden end make_hidden (a_router: WSF_ROUTER) + -- Initialize `router'. + -- Do not display documentation for `a_router'. + require + a_router_attached: a_router /= Void do make (a_router) is_hidden := True + ensure + router_aliased: router = a_router + hidden: is_hidden end router: WSF_ROUTER @@ -46,6 +59,7 @@ feature {NONE} -- Initialization feature -- Documentation mapping_documentation (m: WSF_ROUTER_MAPPING; a_request_methods: detachable WSF_REQUEST_METHODS): WSF_ROUTER_MAPPING_DOCUMENTATION + -- do create Result.make (m) Result.set_is_hidden (is_hidden) @@ -76,4 +90,8 @@ feature -- Execution res.send (m) end +invariant + + router_attached: router /= Void + end diff --git a/library/server/wsf/router/documentation/wsf_self_documented_handler.e b/library/server/wsf/router/documentation/wsf_self_documented_handler.e index 453ee958..ecc23695 100644 --- a/library/server/wsf/router/documentation/wsf_self_documented_handler.e +++ b/library/server/wsf/router/documentation/wsf_self_documented_handler.e @@ -12,7 +12,12 @@ feature -- Documentation mapping_documentation (m: WSF_ROUTER_MAPPING; a_request_methods: detachable WSF_REQUEST_METHODS): WSF_ROUTER_MAPPING_DOCUMENTATION -- Documentation associated with Current handler, in the context of the mapping `m' and methods `a_request_methods'. --| `m' and `a_request_methods' are useful to produce specific documentation when the handler is used for multiple mapping. + require + m_attached: m /= Void + a_request_methods_attached: a_request_methods /= Void deferred + ensure + mapping_documentation_attached: Result /= Void end end diff --git a/library/server/wsf/router/wsf_handler.e b/library/server/wsf/router/wsf_handler.e index 1470a08d..3d15e03f 100644 --- a/library/server/wsf/router/wsf_handler.e +++ b/library/server/wsf/router/wsf_handler.e @@ -11,6 +11,8 @@ feature -- Status report is_valid_context (req: WSF_REQUEST): BOOLEAN -- Is `req' valid context for current handler? + require + req_attached: req /= Void do Result := True end @@ -19,6 +21,8 @@ feature {WSF_ROUTER} -- Mapping on_mapped (a_mapping: WSF_ROUTER_MAPPING; a_rqst_methods: detachable WSF_REQUEST_METHODS) -- Callback called when a router map a route to Current handler + require + a_mapping_attached: a_mapping /= Void do end