From 4f7086a6de38ec62026d81c63926780319f5cc3a Mon Sep 17 00:00:00 2001 From: severin Date: Wed, 12 Mar 2014 17:21:39 +0100 Subject: [PATCH] Updated comments and added contracts for core controls in webcontrol --- .../kernel/webcontrol/wsf_basic_control.e | 20 +++++++---- .../kernel/webcontrol/wsf_button_control.e | 17 ++++++++-- .../kernel/webcontrol/wsf_control.e | 34 +++++++++++++++---- .../webcontrol/wsf_dynamic_multi_control.e | 20 +++++++++-- .../kernel/webcontrol/wsf_form_control.e | 20 ++++++++--- .../webcontrol/wsf_form_element_control.e | 15 ++++++++ .../kernel/webcontrol/wsf_html_control.e | 33 +++++++++++------- .../kernel/webcontrol/wsf_json_object.e | 10 ++++++ .../kernel/webcontrol/wsf_layout_control.e | 17 +++++++--- .../kernel/webcontrol/wsf_multi_control.e | 8 +++-- .../kernel/webcontrol/wsf_page_control.e | 9 ++++- .../kernel/webcontrol/wsf_stateless_control.e | 22 +++++++++--- .../webcontrol/wsf_stateless_multi_control.e | 22 +++++++++--- 13 files changed, 197 insertions(+), 50 deletions(-) diff --git a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_basic_control.e b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_basic_control.e index 99b985a7..fcf4e438 100644 --- a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_basic_control.e +++ b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_basic_control.e @@ -25,24 +25,30 @@ create feature {NONE} -- Initialization - make (t: STRING_32) + make (tag: STRING_32) -- Initialize + require + tag_not_empty: not tag.is_empty do - make_with_body_class (t, "", "", "") + make_with_body_class (tag, "", "", "") end - make_with_body (t, attr, b: STRING_32) + make_with_body (tag, attr, b: STRING_32) -- Initialize with specific attributes and body + require + tag_not_empty: not tag.is_empty do - make_stateless_control (t) + make_stateless_control (tag) attributes := attr body := b end - make_with_body_class (t, attr, c, b: STRING_32) + make_with_body_class (tag, attr, c, b: STRING_32) -- Initialize with specific class, attributes and body + require + tag_not_empty: not tag.is_empty do - make_with_body (t, attr, b) + make_with_body (tag, attr, b) if not c.is_empty then css_classes.extend (c) end @@ -62,6 +68,8 @@ feature -- Change -- Set the body of this control do body := b + ensure + body_set: body = b end feature -- Access diff --git a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_button_control.e b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_button_control.e index bc6d013f..4328786c 100644 --- a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_button_control.e +++ b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_button_control.e @@ -23,12 +23,14 @@ create feature {NONE} -- Initialization make (a_text: STRING_32) - -- Initialize with specified control name and text + -- Initialize with specified text do make_control ("button") add_class ("btn") add_class ("btn-default") text := a_text + ensure + text_set: text = a_text end feature {WSF_PAGE_CONTROL, WSF_CONTROL} -- State management @@ -56,9 +58,14 @@ feature --Event handling -- Set button click event handle do click_event := e + ensure + click_event_set: click_event = e end handle_callback (cname: LIST [STRING_32]; event: STRING_32; event_parameter: detachable ANY) + -- Called if the button is clicked. + require else + cname_has_element: cname.count > 0 do if Current.control_name.same_string (cname [1]) and attached click_event as cevent then cevent.call (Void) @@ -91,20 +98,26 @@ feature -- Change text := t state_changes.replace_with_string (text, "text") end + ensure + text_set: text.same_string (t) end set_disabled (b: BOOLEAN) + -- Enables or disables this component, depending on the value of the parameter b. + -- A disabled button cannot be clicked. do if disabled /= b then disabled := b state_changes.replace_with_boolean (disabled, "disabled") end + ensure + disabled_set: disabled = b end feature -- Properties disabled: BOOLEAN - -- Defines if the button is editable + -- Defines if the button is clickable or not text: STRING_32 -- The text currently displayed on this button diff --git a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_control.e b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_control.e index 42512d45..96ceddd4 100644 --- a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_control.e +++ b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_control.e @@ -1,7 +1,7 @@ note description: "[ - This class is the base class for all stateful controls, like - buttons or forms. + This class is the base class for all stateful controls, like + buttons or forms. ]" author: "" date: "$Date$" @@ -22,22 +22,25 @@ inherit feature {NONE} -- Initialization make (a_tag_name: STRING_32) - -- Initialize with specified and tag + -- Initialize with specified tag require - not a_tag_name.is_empty + a_tag_name_not_empty: not a_tag_name.is_empty do make_stateless_control (a_tag_name) create control_name_prefix.make_empty create state_changes.make create actions.make_array ensure - attached state_changes + state_changes_attached: attached state_changes end feature -- Actions start_modal (url: STRING_32; title: STRING_32; big: BOOLEAN) - --Start a modal window containg an other or the same page + --Start a modal window containing an other or the same page + require + url_not_empty: not url.is_empty + title_not_empty: not title.is_empty local modal: WSF_JSON_OBJECT do @@ -54,6 +57,8 @@ feature -- Actions show_alert (message: STRING_32) --Start a modal window containg an other or the same page + require + message_not_empty: not message.is_empty local alert: WSF_JSON_OBJECT do @@ -65,6 +70,8 @@ feature -- Actions redirect (url: STRING_32) --Redirect to an other page + require + url_not_empty: not url.is_empty local modal: WSF_JSON_OBJECT do @@ -156,6 +163,10 @@ feature -- Rendering end js_class: STRING_32 + -- The js_class is the name of the corresponding javascript class for this control. If this query is not redefined, it just + -- returns the name of the Eiffel class. In case of customized controls, either the according javascript functionality has to + -- be written in a coffeescript class of the same name or this query has to bee redefined and has to return the name of the + -- control Eiffel class of which the javascript functionality should be inherited. do Result := generator end @@ -163,13 +174,14 @@ feature -- Rendering feature -- Event handling handle_callback (cname: LIST [STRING_32]; event: STRING_32; event_parameter: detachable ANY) - -- Method called if any callback received. In this method you can route the callback to the event handler + -- Method called if any callback received. In this method the callback can be routed to the event handler deferred end feature -- Change set_isolation (p: BOOLEAN) + -- Set the isolation state of this control do isolate := p end @@ -177,24 +189,32 @@ feature -- Change feature -- Properties isolate: BOOLEAN + -- The isolation state of this control actions: JSON_ARRAY + -- An array of actions to be carried out, e.g. display a modal (see tutorial for more information about this) control_id: INTEGER assign set_control_id + -- The id of this control set_control_id (d: INTEGER) + -- Set the id of this control do control_id := d end control_name: STRING_32 + -- The name of this control which is composed of the control name prefix and the id of the control do Result := control_name_prefix + control_id.out end control_name_prefix: STRING_32 assign set_control_name_prefix + -- Used to avoid name conflicts since the children stateful controls of stateless controls are appended to the parent + -- control state and therefore could have the same name set_control_name_prefix (p: STRING_32) + -- Set the control name prefix do control_name_prefix := p end diff --git a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_dynamic_multi_control.e b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_dynamic_multi_control.e index 2f3fabcd..f5b0f4aa 100644 --- a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_dynamic_multi_control.e +++ b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_dynamic_multi_control.e @@ -23,13 +23,16 @@ inherit feature {NONE} -- Initialization make_with_tag_name (tag: STRING_32) + -- Initialize with specified tag do Precursor (tag) create items.make_array create pending_removes.make (1) + ensure then + tag_set: tag_name.same_string (tag) end -feature {WSF_DYNAMIC_MULTI_CONTROL} -- Iternal functions +feature {WSF_DYNAMIC_MULTI_CONTROL} -- Internal functions add_control (c: G; id: INTEGER_32) -- Add a control to this multi control @@ -40,9 +43,14 @@ feature {WSF_DYNAMIC_MULTI_CONTROL} -- Iternal functions end max_id := id.max (max_id) items_changed := True + ensure + control_added: controls.has (c) + id_set: attached {WSF_CONTROL} c as d implies d.control_id = id + items_changed: items_changed end execute_pending_removes + -- Execute pending removes local found: BOOLEAN fitem: detachable G @@ -80,12 +88,15 @@ feature {WSF_DYNAMIC_MULTI_CONTROL} -- Iternal functions end items_changed := True end + pending_removes.wipe_out + ensure + pending_removes_empty: pending_removes.is_empty end feature {WSF_PAGE_CONTROL, WSF_CONTROL} -- State management set_state (new_state: JSON_OBJECT) - -- Before we process the callback. We restore the subcontrols + -- Before we process the callback, we restore the subcontrols do if attached {JSON_ARRAY} new_state.item ("items") as new_items then items := new_items @@ -154,6 +165,7 @@ feature end js_class: STRING_32 + -- The default behvaiour of subclasses of the dynamic multi control is that they inherit the javascript functionality of this class do Result := "WSF_DYNAMIC_MULTI_CONTROL" end @@ -161,12 +173,16 @@ feature feature items: JSON_ARRAY + -- Holds the current items in this control pending_removes: ARRAYED_LIST [INTEGER] + -- Stores the removes that have to be executed items_changed: BOOLEAN + -- Indicates whether a change to the controls has happened since the last state readout max_id: INTEGER + -- Largest id of the controls in this multi control invariant all_items_exist: items.count = controls.count diff --git a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_form_control.e b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_form_control.e index 7a342252..df29b0fa 100644 --- a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_form_control.e +++ b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_form_control.e @@ -14,7 +14,7 @@ inherit WSF_STATELESS_MULTI_CONTROL [WSF_STATELESS_CONTROL] rename - make as make_multi_control + make as make_stateless_multi_control redefine add_control end @@ -27,27 +27,35 @@ create feature {NONE} -- Initialization make - -- Initialize + -- Initialize with default label width 2 do make_with_label_width (2) end make_with_label_width (w: INTEGER) + -- Initialize with the specified label width measured in Bootstrap columns + require + w_in_range: w >= 0 and w <= 12 do - make_multi_control + make_stateless_multi_control tag_name := "form" label_width := w add_class ("form-horizontal") + ensure + label_width_set: label_width = w end feature add_control (c: WSF_STATELESS_CONTROL) + -- Add control to this form do Precursor (c) - if attached {WSF_FORM_ELEMENT_CONTROL[detachable ANY]} c as fec then + if attached {WSF_FORM_ELEMENT_CONTROL [detachable ANY]} c as fec then fec.set_label_width (label_width) end + ensure then + control_added: controls.has (c) end feature -- Validation @@ -74,5 +82,9 @@ feature -- Validation feature label_width: INTEGER + -- The label width in this form, measured in Bootstrap columns + +invariant + label_width_in_range: label_width >= 0 and label_width <= 12 end diff --git a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_form_element_control.e b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_form_element_control.e index ccd6730e..2a5c1d15 100644 --- a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_form_element_control.e +++ b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_form_element_control.e @@ -66,18 +66,26 @@ feature -- Modify -- Set the label span (a value between 1 and 12 to specify the bootstrap column span or 0 for not displaying the label) do label_width := w + ensure + label_width_set: label_width = w end feature -- Access value: G + -- Current value of this form element's value control do Result := value_control.value + ensure + result_set: Result = value_control.value end set_value (v: G) + -- Set the value of this form element's value control do value_control.set_value (v) + ensure + value_set: value_control.value = v end feature {WSF_PAGE_CONTROL, WSF_CONTROL} -- State management @@ -98,6 +106,7 @@ feature {WSF_PAGE_CONTROL, WSF_CONTROL} -- State management end full_state: WSF_JSON_OBJECT + -- The full state of this form local controls_state: WSF_JSON_OBJECT do @@ -147,6 +156,8 @@ feature -- Event handling handle_callback (cname: LIST [STRING_32]; event: STRING_32; event_parameter: detachable ANY) -- Pass callback to subcontrols + require else + cname_not_empty: cname.count > 0 do if cname [1].same_string (control_name) then cname.go_i_th (1) @@ -186,6 +197,8 @@ feature -- Validation -- Add an additional validator that will check the input of the value control of this form element control on validation do validators.extend (v) + ensure + validator_added: validators.has (v) end set_error (e: STRING_32) @@ -193,6 +206,8 @@ feature -- Validation do error := e state_changes.replace (create {JSON_STRING}.make_json (e), "error") + ensure + error_set: error.same_string (e) end validate diff --git a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_html_control.e b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_html_control.e index 10b6e369..9c18c981 100644 --- a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_html_control.e +++ b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_html_control.e @@ -23,17 +23,21 @@ create feature {NONE} -- Initialization - make (t, v: STRING_32) - -- Initialize + make (tag, v: STRING_32) + -- Initialize with specified tag and HTML value + require + tag_not_empty: not tag.is_empty do - make_value_control (t) + make_value_control (tag) html := v + ensure + html_set: html.same_string (v) end feature {WSF_PAGE_CONTROL, WSF_CONTROL} -- State management set_state (new_state: JSON_OBJECT) - -- Restore html from json + -- Restore HTML from json do if attached {JSON_STRING} new_state.item ("html") as new_html then html := new_html.unescaped_string_32 @@ -50,6 +54,7 @@ feature {WSF_PAGE_CONTROL, WSF_CONTROL} -- State management feature --Event handling handle_callback (cname: LIST [STRING_32]; event: STRING_32; event_parameter: detachable ANY) + -- By default, this does nothing do end @@ -61,26 +66,28 @@ feature -- Implementation Result := render_tag (html, "") end - set_html (t: STRING_32) - do - if not t.same_string (html) then - html := t - state_changes.replace_with_string (html, "html") - end - end - value: STRING_32 + -- The HTML value of this HTML control do Result := html + ensure then + result_set: Result.same_string (html) end set_value (v: STRING_32) + -- Set HTML value of this control do - html := v + if not v.same_string (html) then + html := v + state_changes.replace_with_string (html, "html") + end + ensure then + html_set: html.same_string (v) end feature -- Properties html: STRING_32 + -- The HTML value of this HTML control end diff --git a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_json_object.e b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_json_object.e index f465256b..5b43148e 100644 --- a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_json_object.e +++ b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_json_object.e @@ -32,6 +32,8 @@ feature create l_value.make_json_from_string_32 (a_value.as_string_32) end put (l_value, key) + ensure + has_key: has_key (key) end put_integer (value: detachable INTEGER_64; key: JSON_STRING) @@ -46,6 +48,8 @@ feature create l_value.make_integer (a_value) end put (l_value, key) + ensure + has_key: has_key (key) end put_natural (value: detachable NATURAL_64; key: JSON_STRING) @@ -60,6 +64,8 @@ feature create l_value.make_natural (a_value) end put (l_value, key) + ensure + has_key: has_key (key) end put_real (value: detachable DOUBLE; key: JSON_STRING) @@ -74,6 +80,8 @@ feature create l_value.make_real (a_value) end put (l_value, key) + ensure + has_key: has_key (key) end put_boolean (value: detachable BOOLEAN; key: JSON_STRING) @@ -88,6 +96,8 @@ feature create l_value.make_boolean (a_value) end put (l_value, key) + ensure + has_key: has_key (key) end replace_with_string (value: detachable READABLE_STRING_GENERAL; key: JSON_STRING) diff --git a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_layout_control.e b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_layout_control.e index a4375f7e..68bd1760 100644 --- a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_layout_control.e +++ b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_layout_control.e @@ -1,7 +1,7 @@ note description: "[ - A lightweight layout container to encapsulate the grid layout - provided by bootstrap. + A lightweight layout container to encapsulate the grid layout + provided by bootstrap. ]" author: "" date: "$Date$" @@ -14,7 +14,7 @@ inherit WSF_STATELESS_MULTI_CONTROL [WSF_STATELESS_CONTROL] rename - make as make_multi_control, + make as make_stateless_multi_control, add_control as add_control_raw end @@ -23,7 +23,8 @@ create feature {NONE} -- Initialization - make (n: STRING_32) + make + --Initialize do make_with_tag_name ("div") add_class ("row") @@ -32,6 +33,10 @@ feature {NONE} -- Initialization feature -- Add control add_control_with_offset (c: WSF_STATELESS_CONTROL; span, offset: INTEGER) + -- Add a control as column with the specified span and offset + require + offset_in_range: offset >= 0 and offset <= 12 + span_in_range: span >= 0 and span <= 12 - offset local div: WSF_STATELESS_MULTI_CONTROL [WSF_STATELESS_CONTROL] do @@ -42,6 +47,7 @@ feature -- Add control end add_control (col: INTEGER; c: WSF_STATELESS_CONTROL) + -- Add a control to the specified column require col >= 1 and col <= controls.count attached {WSF_STATELESS_MULTI_CONTROL [WSF_STATELESS_CONTROL]} controls [col] @@ -52,6 +58,9 @@ feature -- Add control end add_column (span: INTEGER) + -- Add a multi control as Bootstrap column with the specified span + require + span_in_range: span >= 0 and span <= 12 local div: WSF_STATELESS_MULTI_CONTROL [WSF_STATELESS_CONTROL] do diff --git a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_multi_control.e b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_multi_control.e index 2c237abe..45a90e61 100644 --- a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_multi_control.e +++ b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_multi_control.e @@ -27,16 +27,20 @@ create feature {NONE} -- Initialization make - -- Initialize with specified control name and default tag "div" + -- Initialize with default tag "div" do make_with_tag_name ("div") end make_with_tag_name (t: STRING_32) - -- Initialize with specified control name and tag + -- Initialize with specified tag + require + t_not_empty: not t.is_empty do make_control (t) controls := create {ARRAYED_LIST [G]}.make (5); + ensure + tag_name_set:tag_name.same_string (t) end feature {WSF_PAGE_CONTROL, WSF_CONTROL} -- State management diff --git a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_page_control.e b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_page_control.e index 4438c3ac..143d451f 100644 --- a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_page_control.e +++ b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_page_control.e @@ -38,6 +38,8 @@ feature {NONE} -- Initialization request := req response := res initialize_controls + ensure + base_path_set: base_path.same_string (a_base_path) end feature -- Access @@ -107,7 +109,7 @@ feature -- Implementation end render_page - -- Render and send the HTML Page + -- Render and send the HTML page local page: WSF_PAGE_RESPONSE do @@ -118,6 +120,7 @@ feature -- Implementation end render: STRING_32 + -- Render the HTML page local ajax: BOOLEAN do @@ -183,6 +186,7 @@ feature -- Event handling feature {WSF_PAGE_CONTROL, WSF_CONTROL} -- State management state: WSF_JSON_OBJECT + -- State of the page do create Result.make Result.put_string (control_name, "id") @@ -191,6 +195,7 @@ feature {WSF_PAGE_CONTROL, WSF_CONTROL} -- State management end set_state (sp: JSON_OBJECT) + -- Set state do if attached {JSON_OBJECT} sp.item ("controls") as ct and then attached {JSON_OBJECT} ct.item (control.control_name) as value_state then control.load_state (value_state) @@ -211,8 +216,10 @@ feature {WSF_PAGE_CONTROL, WSF_CONTROL} -- State management feature control_name: STRING_32 + -- Name of this page base_path: STRING_32 + -- The base path of the assets files feature {NONE} -- Root control diff --git a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_stateless_control.e b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_stateless_control.e index 8b5c2a47..4d73e8dc 100644 --- a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_stateless_control.e +++ b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_stateless_control.e @@ -17,7 +17,7 @@ feature {NONE} -- Initialization make (a_tag_name: STRING_32) -- Initialize with specified tag require - not a_tag_name.is_empty + a_tag_name_not_empty: not a_tag_name.is_empty do tag_name := a_tag_name create css_classes.make (0) @@ -38,18 +38,29 @@ feature -- Change add_class (c: STRING_32) -- Add a css class to this control + require + c_not_empty: not c.is_empty do css_classes.force (c) + ensure + class_added: css_classes.has (c) end - remove_class (cla: STRING_32) - -- Add a css class to this control + remove_class (c: STRING_32) + -- Remove a css class from this control + require + c_not_empty: not c.is_empty do - css_classes.prune (cla) + css_classes.start + css_classes.prune_all (c) + ensure + c_removed: not css_classes.has (c) end append_attribute (a: STRING_32) -- Adds the specified attribute to the attribute string of this control + require + a_not_empty: not a.is_empty do if attached attributes as attr then attr.append (" ") @@ -110,4 +121,7 @@ feature -- Rendering deferred end +invariant + tag_name_not_empty: not tag_name.is_empty + end diff --git a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_stateless_multi_control.e b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_stateless_multi_control.e index 84a7914a..4444f1eb 100644 --- a/draft/library/wsf_js_widget/kernel/webcontrol/wsf_stateless_multi_control.e +++ b/draft/library/wsf_js_widget/kernel/webcontrol/wsf_stateless_multi_control.e @@ -1,8 +1,8 @@ note description: "[ - Mutli controls are used as containers for multiple controls, for - example a form is a multi control. - ]" + Mutli controls are used as containers for multiple controls, for + example a form is a multi control. + ]" author: "" date: "$Date$" revision: "$Revision$" @@ -13,6 +13,8 @@ class inherit WSF_MULTI_CONTROL [G] + rename + make as make_multi_control redefine add_control, set_control_name_prefix, @@ -22,11 +24,12 @@ inherit end create - make_with_tag_name, make_tag_less + make_with_tag_name, make feature {NONE} -- Initialization - make_tag_less + make + -- Initialize do make_with_tag_name ("") stateless := True @@ -35,18 +38,25 @@ feature {NONE} -- Initialization feature set_control_id (d: INTEGER) + -- Set id of this control and update subcontrol prefixes do control_id := d set_subcontrol_prefixes + ensure then + control_id_set: control_id.abs = d end set_control_name_prefix (p: STRING_32) + -- Set control name prefix of this control do control_name_prefix := p set_subcontrol_prefixes + ensure then + control_name_prefix_set: control_name_prefix.same_string (p) end set_subcontrol_prefixes + -- Update subcontrol prefixes do across controls as e @@ -67,6 +77,8 @@ feature d.control_id := controls.count d.control_name_prefix := control_name_prefix + control_id.out + "_" end + ensure then + control_added: controls.has (c) end render_tag (body: STRING_32; attrs: detachable STRING_32): STRING_32