+
Point of view
XML_DTD_PARSER
expanded class XML_DTD_PUBLIC_REPOSITORY
- Direct parents
- insert list: ANY
require
-
valid_public_id: not public_id.is_empty
-
valid_local_path: not local_path.is_empty
-
not_registered: not is_registered(public_id)
-
file_exists: (create {FILE_TOOLS}).file_exists(local_path)
ensure
require
-
valid_public_id: not public_id.is_empty
require
- not public_id.is_empty
- not is_registered(public_id) implies not url.is_empty
ensure
-
connected_or_void_stream: Result /= Void implies Result.is_connected
-
not_connected_is_error: Result = Void implies last_error /= Void