| 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) |
| 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) |