made deleted into an effective routine
This commit is contained in:
@@ -297,14 +297,6 @@ feature -- DELETE
|
||||
end
|
||||
end
|
||||
|
||||
deleted (req: WSF_REQUEST): BOOLEAN
|
||||
-- Has resource named by `req' been deleted?
|
||||
do
|
||||
if not req.error_handler.has_error then
|
||||
Result := True
|
||||
end
|
||||
end
|
||||
|
||||
delete_queued (req: WSF_REQUEST): BOOLEAN
|
||||
-- Has resource named by `req' been queued for deletion?
|
||||
do
|
||||
|
||||
@@ -197,7 +197,12 @@ feature -- DELETE
|
||||
-- Has resource named by `req' been deleted?
|
||||
require
|
||||
req_attached: req /= Void
|
||||
deferred
|
||||
do
|
||||
if not req.error_handler.has_error then
|
||||
Result := True
|
||||
end
|
||||
ensure
|
||||
negative_implication: not Result implies req.error_handler.has_error
|
||||
end
|
||||
|
||||
delete_queued (req: WSF_REQUEST): BOOLEAN
|
||||
|
||||
Reference in New Issue
Block a user