Updated comments and added contracts for core controls in webcontrol

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

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

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
+		This class is the base class for all stateful controls, like
-			buttons or forms.
+		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

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

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

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

draft/library/wsf_js_widget/kernel/webcontrol/wsf_html_control.e

@@ -23,17 +23,21 @@ create
 
 feature {NONE} -- Initialization
 
-	make (t, v: STRING_32)
+	make (tag, v: STRING_32)
-			-- Initialize
+			-- 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

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)

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
+		A lightweight layout container to encapsulate the grid layout
-			provided by bootstrap.
+		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

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

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
 

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)
+	remove_class (c: STRING_32)
-			-- Add a css class to this control
+			-- 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

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
+		Mutli controls are used as containers for multiple controls, for
-			example a form is a multi control.
+		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