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) |
deferred really_append_in (buffer: STRING, stop_at_dot: BOOLEAN, stopped: BOOLEAN): BOOLEAN |
require
ensure
|
deferred really_to_html_stream (html: HTML_OUTPUT_STREAM, stop_at_dot: BOOLEAN, stopped: BOOLEAN): BOOLEAN |
require
ensure
|