class HTML_OUTPUT_STREAM

All features

Highly tailored filter that outputs well-formed HTML. Be aware that you cannot add any character as you want. You can filter this stream, but keep it available because it controls the tags.

Direct parents

conformant parents

FILTER_OUTPUT_STREAM

Summary

creation features

exported features

CGI extensions: written before the HTML itself is open

Main HTML structure

Attributes management

Putting characters

Header tags

Frames

Body tags

Forms

State queries

States

Send to the underlying stream

Once strings

To write a number:

Other features:

Details

connect_to (a_stream: OUTPUT_STREAM)

Connect the filter to some underlying stream.

require

  • not is_connected
  • a_stream.is_connected
  • not a_stream.is_filtered

ensure

  • is_connected

put_cgi_header (key: STRING, value: STRING)

require

  • not started
  • key /= Void
  • value /= Void

ensure

  • has_cgi_header

header

require

  • not started

ensure

  • in_header

body

require

  • in_header

ensure

  • in_body

frames

require

  • in_header

ensure

  • in_frames

close

require

  • in_body or else in_frames

ensure

  • finished

last_tag: STRING

require

  • started and then not finished
  • has_open_tag

ensure

  • Result /= Void

has_open_tag: BOOLEAN

ensure

  • Result implies started and then not finished

attributes: STRING

Because there are so many attributes for each tag, we did not want features with scores of parameters. So, we decided to have a general-purpose with_attribute feature to be called before a tag creation.

Typical use:

html_out.with_attribute(once "width", once "80%%") html_out.with_attribute(once "align", once "center") html_out.with_attribute(once "valign", once "top") html_out.open_table_cell

with_attribute (name: STRING, value: STRING)

Call this feature before adding an opening tag; all the attributes will be added to the tag.

open_tag (tag: STRING)

ensure

  • tags.count = old tags.count + 1
  • last_tag.same_as(tag)

open_close_tag (tag: STRING)

ensure

  • tags.count = old tags.count

close_tag (tag: STRING)

require

  • tags.count > 0
  • last_tag.same_as(tag)

ensure

  • tags.count = old tags.count - 1

filtered_put_character (c: CHARACTER)

require

  • is_connected
  • can_put_character(c)

filtered_flush

require

  • is_connected

can_put_character (c: CHARACTER): BOOLEAN
put_entity (entity: STRING)

require

  • started
  • not finished
  • not entity.has(';')
  • not entity.has('&')
  • not entity.has('<')
  • not entity.has('>')

put_comment (comment: STRING)
indent

require

  • started
  • not finished

put_base (base: STRING)

require

  • in_header

put_meta (equiv: STRING, content: STRING)

require

  • in_header

put_stylesheet (ref: STRING)

require

  • in_header

open_title

require

  • in_header

close_title

require

  • in_header
  • last_tag.same_as(os_title)

put_script (language: STRING, source: STRING)

require

  • in_header
  • language /= Void
  • source /= Void

open_script (language: STRING)

require

  • in_header
  • language /= Void

close_script

require

  • in_script
  • last_tag.same_as(os_script)

open_frameset

require

  • in_frames or else in_frameset

ensure

  • in_frameset

close_frameset

require

  • in_frameset

ensure

  • in_frames or else in_frameset

put_frame (src: STRING, name: STRING)

require

  • in_frameset
  • src /= Void

ensure

  • in_frameset

open_noframes

require

  • in_frames

ensure

  • in_noframes

close_noframes

require

  • in_noframes

ensure

  • in_frames

open_section

require

  • in_a_body

close_section

require

  • in_a_body
  • last_tag.same_as(os_h1)

open_subsection

require

  • in_a_body

close_subsection

require

  • in_a_body
  • last_tag.same_as(os_h2)

open_subsubsection

require

  • in_a_body

close_subsubsection

require

  • in_a_body
  • last_tag.same_as(os_h3)

put_break

require

  • in_a_body

put_horizontal_rule

require

  • in_a_body

put_image (source: STRING)

require

  • in_a_body
  • source /= Void

open_bold

require

  • in_a_body

close_bold

require

  • in_a_body
  • last_tag.same_as(os_b)

open_font (size: STRING)

require

  • in_a_body

close_font

require

  • in_a_body
  • last_tag.same_as(os_font)

open_italics

require

  • in_a_body

close_italics

require

  • in_a_body
  • last_tag.same_as(os_i)

open_underlined

require

  • in_a_body

close_underlined

require

  • in_a_body
  • last_tag.same_as(os_u)

open_typeset

require

  • in_a_body

close_typeset

require

  • in_a_body
  • last_tag.same_as(os_tt)

open_anchor_address (ref: STRING, target: STRING)

require

  • in_a_body
  • ref /= Void

open_anchor_name (ref: STRING)

require

  • in_a_body
  • ref /= Void

close_anchor

require

  • in_a_body
  • last_tag.same_as(os_a)

open_list

require

  • in_a_body

ensure

  • in_list

open_numbered_list

require

  • in_a_body

ensure

  • in_list

close_list

require

  • in_list
  • last_tag.same_as(os_ul) or else last_tag.same_as(os_ol)

ensure

  • in_a_body

open_list_item

require

  • in_list

ensure

  • in_list_item

close_list_item

require

  • in_list_item
  • last_tag.same_as(os_li)

ensure

  • in_list

open_table

require

  • in_a_body

ensure

  • in_table

close_table

require

  • in_table
  • last_tag.same_as(os_table)

ensure

  • in_a_body

open_table_row

require

  • in_table

ensure

  • in_table_row

close_table_row

require

  • in_table_row
  • last_tag.same_as(os_tr)

ensure

  • in_table

open_table_cell

require

  • in_table_row

ensure

  • in_table_cell

close_table_cell

require

  • in_table_cell
  • last_tag.same_as(os_td)

ensure

  • in_table_row

open_form (name: STRING, method: STRING, action: STRING)

require

  • in_a_body
  • name /= Void
  • action /= Void
  • method.same_as(os_method_get) or else method.same_as(os_method_post)

ensure

  • in_form

close_form

require

  • in_form
  • last_tag.same_as(os_form)

open_text_area (name: STRING, rows: INTEGER, cols: INTEGER)

require

  • in_a_form
  • name /= Void
  • rows > 0
  • cols > 0

ensure

  • in_text_area

close_text_area

require

  • in_text_area

put_validate_button (name: STRING, title: STRING)

require

  • in_a_form
  • name /= Void

put_reset_button (name: STRING, title: STRING)

require

  • in_a_form
  • name /= Void

put_hidden_field (name: STRING, value: STRING)

require

  • in_a_form
  • name /= Void

put_text_field (name: STRING, value: STRING)

require

  • in_a_form
  • name /= Void

put_radio_button (name: STRING, value: STRING, checked: BOOLEAN)

require

  • in_a_form
  • name /= Void
  • value /= Void

put_check_box (name: STRING, value: STRING, checked: BOOLEAN)

require

  • in_a_form
  • name /= Void
  • value /= Void

open_combo_select (name: STRING)

require

  • in_a_form
  • name /= Void

ensure

  • in_select

open_multiple_select (name: STRING, size: INTEGER)

require

  • in_a_form
  • name /= Void
  • size > 0

ensure

  • in_select

close_select

require

  • in_select
  • last_tag.same_as(os_select)

ensure

  • in_a_form

open_option (value: STRING)

require

  • in_select

ensure

  • in_option

close_option

require

  • in_option
  • last_tag.same_as(os_option)

ensure

  • in_select

open_paragraph

require

  • in_a_body

ensure

  • in_paragraph

close_paragraph

require

  • in_paragraph

ensure

  • in_a_body

open_preformatted

require

  • in_a_body

ensure

  • in_preformatted

close_preformatted

require

  • in_preformatted
  • last_tag.same_as(os_pre)

open_blockquote

require

  • in_a_body

ensure

  • in_blockquote

close_blockquote

require

  • in_blockquote

ensure

  • in_a_body

open_div

require

  • in_a_body

ensure

  • in_div

close_div

require

  • in_div

ensure

  • in_a_body

put_input (type: STRING, name: STRING, value: STRING, checked: BOOLEAN)
started: BOOLEAN
finished: BOOLEAN
in_header: BOOLEAN
in_script: BOOLEAN
in_body: BOOLEAN
in_list: BOOLEAN
in_list_item: BOOLEAN
in_table: BOOLEAN
in_table_row: BOOLEAN
in_table_cell: BOOLEAN
in_form: BOOLEAN
in_select: BOOLEAN
in_option: BOOLEAN
in_frames: BOOLEAN
in_frameset: BOOLEAN
in_noframes: BOOLEAN
in_a_body: BOOLEAN
in_a_form: BOOLEAN
in_text_area: BOOLEAN
in_paragraph: BOOLEAN
in_blockquote: BOOLEAN
in_div: BOOLEAN
in_preformatted: BOOLEAN
state: INTEGER
set_state (a_state: INTEGER)

ensure

  • states.count = old states.count + 1

reset_state (a_state: INTEGER)

require

  • state = a_state

ensure

  • states.count = old states.count - 1

state_closed: INTEGER
state_in_header: INTEGER
state_in_script: INTEGER
state_in_body: INTEGER
state_in_list: INTEGER
state_in_list_item: INTEGER
state_in_table: INTEGER
state_in_table_row: INTEGER
state_in_table_cell: INTEGER
state_in_text_area: INTEGER
state_in_paragraph: INTEGER
state_in_blockquote: INTEGER
state_in_div: INTEGER
state_in_pre: INTEGER
state_in_form: INTEGER
state_in_select: INTEGER
state_in_option: INTEGER
state_in_frames: INTEGER
state_in_frameset: INTEGER
state_in_noframes: INTEGER
state_over: INTEGER
pipe_character (c: CHARACTER)

Put the character down the pipe.

pipe_string (s: STRING)

Put the whole string down the pipe.

pipe_quoted_string (quoted: STRING)
quote_quotes (quoted: STRING, in: STRING)

Internal transformation in tag attributes

connect_to (a_stream: OUTPUT_STREAM)

Connect the filter to some underlying stream.

require

  • not is_connected
  • a_stream.is_connected
  • not a_stream.is_filtered

ensure

  • is_connected

local_can_disconnect: BOOLEAN

True if this stream can be safely disconnected (without data loss, etc.) without taking into account the state of the underlying stream.

tags: FAST_ARRAY [E_][STRING]
states: FAST_ARRAY [E_][INTEGER]
has_cgi_header: BOOLEAN

are there any CGI headers before the HTML itself is inserted?

last_character_is_new_line: BOOLEAN

True if the last put character was a '%N'

os_key_colon: STRING
os_html_header: STRING
os_html_body_start: STRING
os_html_body_footer: STRING
os_html_frames_footer: STRING
os_start_comment: STRING
os_end_comment: STRING
os_entity_quot: STRING
os_entity_lt: STRING
os_entity_gt: STRING
os_entity_amp: STRING
os_base: STRING
os_end_open_close_tag_attrib: STRING
os_meta_equiv: STRING
os_attrib_content: STRING
os_stylesheet: STRING
os_title: STRING
os_script_begin: STRING
os_attrib_src: STRING
os_script_end: STRING
os_language: STRING
os_script: STRING
os_h1: STRING
os_h2: STRING
os_h3: STRING
os_br: STRING
os_hr: STRING
os_img: STRING
os_src: STRING
os_b: STRING
os_i: STRING
os_u: STRING
os_tt: STRING
os_size: STRING
os_font: STRING
os_pre: STRING
os_href: STRING
os_target: STRING
os_name: STRING
os_a: STRING
os_ul: STRING
os_ol: STRING
os_li: STRING
os_table: STRING
os_tr: STRING
os_td: STRING
os_method_get: STRING
os_method_post: STRING
os_method: STRING
os_action: STRING
os_form: STRING
os_rows: STRING
os_cols: STRING
os_textarea: STRING
os_submit: STRING
os_reset: STRING
os_hidden: STRING
os_text: STRING
os_radio: STRING
os_checkbox: STRING
os_select: STRING
os_multiple: STRING
os_value: STRING
os_option: STRING
os_type: STRING
os_checked: STRING
os_input: STRING
os_frameset: STRING
os_frame: STRING
os_noframes: STRING
os_paragraph: STRING
os_blockquote: STRING
os_div: STRING
os: STRING

used as a buffer

disconnect

Disconnect from the underlying stream.

require

  • is_connected
  • can_disconnect
  • is_connected
  • can_disconnect

ensure

  • not is_connected
  • stream = Void
  • not is_filtered

do_detach

Used by the underlying stream to require not to be filtered anymore

stream: OUTPUT_STREAM

The underlying stream (i.e. the filtered one)

put_character (c: CHARACTER)

require

  • is_connected
  • not is_filtered and then can_put_character(c)

flush

Flushes the pipe. If is_filtered, calls the filter's flush instead.

require

  • is_connected

detach

Shake off the filter.

ensure

  • not is_filtered

filter: FILTER_OUTPUT_STREAM

The filter that uses this stream as backend

deferred is_connected: BOOLEAN

True if the stream is connected. Only in that case can data be transfered via this stream.

deferred disconnect

Try to disconnect the stream. Note that it *does not* ensure that the stream will effectively be disconnected (some terminal streams, for instance, are always connected) but the feature can be used to "shake off" filters.

require

  • is_connected
  • can_disconnect

ensure

  • not is_filtered

is_filtered: BOOLEAN

True if some filter is using this stream as backend. use that filter instead.

deferred detach

Shake off the filter.

ensure

  • not is_filtered

descriptor: INTEGER

Some OS-dependent descriptor. Mainly used by the sequencer library (see READY_CONDITION).

require

  • is_connected
  • has_descriptor

has_descriptor: BOOLEAN

True if that stream can be associated to some OS-meaningful descriptor.

require

  • is_connected

deferred can_disconnect: BOOLEAN

True if the stream can be safely disconnected (without data loss, etc.)

require

  • is_connected

stream_pointer: POINTER

Some Back-end-dependent pointer (FILE* in C, InputStream or OutputStream in Java)

require

  • is_connected
  • has_stream_pointer

has_stream_pointer: BOOLEAN

True if that stream can be associated to some Back-end-meaningful stream pointer.

require

  • is_connected

set_filter (a_filter: FILTER)

Used by the filter itself to get attached

require

  • a_filter /= Void

ensure

  • filter = a_filter

filter: FILTER

The filter that uses this stream as backend

deferred filtered_descriptor: INTEGER

Find the descriptor of the terminal stream... Filters do not have descriptors of their own

require

  • is_connected
  • filtered_has_descriptor

deferred filtered_has_descriptor: BOOLEAN

True if the underlying terminal stream has a descriptor

require

  • is_connected

deferred filtered_stream_pointer: POINTER

Find the pointer of the terminal stream... Filters do not have pointers of their own

require

  • is_connected
  • filtered_has_stream_pointer

deferred filtered_has_stream_pointer: BOOLEAN

True if the underlying terminal stream has a pointer

require

  • is_connected

sequencer_descriptor (file: POINTER): INTEGER
deferred put_character (c: CHARACTER)

require

  • is_connected
  • not is_filtered and then can_put_character(c)

deferred flush

Flushes the pipe. If is_filtered, calls the filter's flush instead.

require

  • is_connected

deferred can_put_character (c: CHARACTER): BOOLEAN
deferred is_filtered: BOOLEAN
deferred is_connected: BOOLEAN
put_string (s: STRING)

Output s to current output device.

require

  • is_connected
  • not is_filtered
  • s /= Void

put_unicode_string (unicode_string: UNICODE_STRING)

Output the UTF-8 encoding of the unicode_string.

require

  • is_connected
  • not is_filtered
  • unicode_string /= Void

put_line (s: STRING)

Output the string followed by a '%N'.

frozen put_integer (i: INTEGER_64)

Output i to current output device.

require

  • is_connected
  • not is_filtered

frozen put_integer_format (i: INTEGER_64, s: INTEGER)

Output i to current output device using at most s character.

require

  • is_connected
  • not is_filtered

put_real (r: REAL)

Output r to current output device.

require

  • is_connected
  • not is_filtered

put_real_format (r: REAL, f: INTEGER)

Output r with only f digit for the fractionnal part. Examples:

   put_real(3.519,2) print "3.51".

require

  • is_connected
  • not is_filtered
  • f >= 0

put_double (d: REAL)
This feature is obsolete: Now use `put_real' (October 2004).
put_double_format (d: REAL, f: INTEGER)
This feature is obsolete: Now use `put_real_format' (October 2004).
put_real_scientific (r: REAL, f: INTEGER)

Output r using the scientific notation with only f digit for the fractionnal part. Examples:

   put_real_scientific(3.519,2) print "3.16e+00".

require

  • is_connected
  • not is_filtered
  • f >= 0

put_number (number: NUMBER)

Output the number.

require

  • is_connected
  • not is_filtered
  • number /= Void

put_boolean (b: BOOLEAN)

Output b to current output device according to the Eiffel format.

require

  • is_connected
  • not is_filtered

put_pointer (p: POINTER)

Output a viewable version of p.

require

  • is_connected
  • not is_filtered

put_new_line

Output a newline character.

require

  • is_connected
  • not is_filtered

put_spaces (nb: INTEGER)

Output nb spaces character.

require

  • is_connected
  • not is_filtered
  • nb >= 0

append_file (file_name: STRING)

require

  • is_connected
  • not is_filtered
  • (create {FILE_TOOLS}.default_create).is_readable(file_name)

tmp_file_read: TEXT_FILE_READ
tmp_string: STRING
io_putc (byte: CHARACTER, stream: POINTER)
io_fwrite (buf: NATIVE_ARRAY [E_][CHARACTER], size: INTEGER, stream: POINTER)
io_flush (stream: POINTER)
is_connected: BOOLEAN

True if the filter is connected to some underlying stream.

deferred disconnect

Disconnect from the underlying stream.

require

  • is_connected
  • can_disconnect

ensure

  • not is_connected
  • stream = Void

can_disconnect: BOOLEAN
filtered_descriptor: INTEGER
filtered_has_descriptor: BOOLEAN
filtered_stream_pointer: POINTER
filtered_has_stream_pointer: BOOLEAN

Class invariant