+
Point of view
All features
class XMLNS_TREE
Features
{}
- with_attribute (attribute_namespace: UNICODE_STRING, attribute_name: UNICODE_STRING, attribute_value: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)
- open_node (node_namespace: UNICODE_STRING, node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)
- close_node (node_namespace: UNICODE_STRING, node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)
- open_close_node (node_namespace: UNICODE_STRING, node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)
- xml_header (line: INTEGER_32, column: INTEGER_32)
- processing_instruction (a_target: UNICODE_STRING, a_data: UNICODE_STRING)
- current_node: UNICODE_STRING
- current_namespace: UNICODE_STRING
- entity (a_entity: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32): UNICODE_STRING
- data (a_data: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)
- parse_error (line: INTEGER_32, column: INTEGER_32, message: STRING)
- at_error: BOOLEAN
{}
{}
require
- target /= Void
- processor /= Void
require
- not attribute_name.is_empty
- attribute_value /= Void
require
ensure
- not at_error implies current_node.is_equal(node_name)
- not at_error implies current_namespace = node_namespace or else node_namespace /= Void and then current_namespace /= Void and then current_namespace.is_equal(node_namespace)
require
- not node_name.is_empty
- current_node.is_equal(node_name)
- node_namespace = Void implies current_namespace = Void
- node_namespace /= Void implies current_namespace.is_equal(node_namespace)
require
- url.is_connected implies url.read