make (a_name: STRING, a_parent: HTML_NODE) |
name: STRING |
attributes_count: INTEGER |
children_count: INTEGER |
attribute (i: INTEGER): HTML_ATTRIBUTE |
require
|
child (i: INTEGER): HTML_ELEMENT |
require
|
really_append_in (buffer: STRING, stop_at_dot: BOOLEAN, stopped: BOOLEAN): BOOLEAN |
require
ensure
|
really_to_html_stream (html: HTML_OUTPUT_STREAM, stop_at_dot: BOOLEAN, stopped: BOOLEAN): BOOLEAN |
require
ensure
|
add_child (a_child: HTML_ELEMENT) |
add_attribute (attr_name: STRING, attr_value: STRING) |
make (a_name: STRING, a_parent: HTML_NODE) |
attributes: FAST_ARRAY [E_][HTML_ATTRIBUTE] |
children: FAST_ARRAY [E_][HTML_ELEMENT] |
parent: HTML_NODE |
to_string: STRING |
append_in (buffer: STRING, stop_at_dot: BOOLEAN) |
to_html_stream (html: HTML_OUTPUT_STREAM, stop_at_dot: BOOLEAN) |