note

	description: "EiffelVision widget manager"
	legal: "See notice at end of class.";
	status: "See notice at end of class.";
	date: "$Date$";
	revision: "$Revision$"

class
	W_MANAGER 

inherit

	G_ANY
		export
			{NONE} all
		undefine
			is_equal, copy
		end;

	ASCII
		export
			{NONE} all
		undefine
			is_equal, copy
		end;

	ARRAY [WIDGET]
		rename
			make as array_make,
			count as array_count,
			empty as array_empty,
			item as i_th
		export
			{NONE} all;
			{ANY} has, i_th, valid_index, area
		end

create

	make

feature {NONE} -- Initialization

	make
			-- Create a widget manager.
		do
			array_make (1, 100)
		end;

feature -- Access

	last_inserted_position: INTEGER;
			-- Index position of last widget inserted into Current

	item: WIDGET
			-- Item at cursor position
		require
			not_off: not off
		do
			Result := area.item (index - 1)
		ensure
			valid_result: Result /= Void
		end;

feature -- Status report

	after: BOOLEAN
			-- Is there no valid cursor position 
			-- to the right of cursor?
		do
			Result := index = count + 1
		end;

	before: BOOLEAN
			-- Is there no valid cursor position 
			-- to the left of cursor?
		do
			Result := index = 0
		end;

	off: BOOLEAN
		do
			Result := after or else before
		end;

feature -- Measurement

	count: INTEGER;
			-- Number of widgets in Current

feature -- Cursor movement
  
	back
			-- Move cursor back one position.
		require
			not_before: not before
		do
			index := index - 1
		ensure
			moved_back: index = old index - 1
		end;

	finish
			-- Move cursor to end position
		do
			index := count
		end

	forth
			-- Move cursor forward one position.
		require
			not_after: not after
		do
			index := index + 1
		ensure
			moved_forth: index = old index + 1
		end;

	start
			-- Move cursor to first position.
		do
			index := 1
		end;

feature -- Basic operations

	new (widget, a_parent: WIDGET)
			-- Add `widget' to the list as a child of `parent'.
		require
			widget_exists: widget /= Void;
			a_parent_exists_unless_depth_null: (a_parent = Void) 
								implies (widget.depth = 0);
			depth_not_null_unless_parent_exists: (widget.depth > 0) 
								implies (a_parent /= Void);
			has_parent: (a_parent /= Void) implies has (a_parent);
		local
			insert_position, i: INTEGER;
			widget_area: like area;
			moved_widget: WIDGET;
		do
			check
				implementation_not_created: widget.implementation = Void;
			end
			if widget.depth = 0 then
				if count >= array_count then
					conservative_resize (1, array_count + Chunk)
				end;
				area.put (widget, count);
				count := count + 1;
				last_inserted_position := count;
			else
				insert_position := index_of (a_parent) + 1;
				if count + 1 > array_count then
						-- Resize Current if necessary
					conservative_resize (1, array_count + Chunk)
				end;
				widget_area := area;
				from
						-- Shift widgets by one for widget insertion
					i := count - 1
				until
					i < insert_position
				loop
					moved_widget := widget_area.item (i);
					widget_area.put (moved_widget, i + 1);
					if moved_widget.implementation /= Void then
						moved_widget.implementation.set_widget_index (i + 2);
					end;
					i := i - 1
				end;
				count := count + 1;
				widget_area.put (widget, insert_position);
				last_inserted_position := insert_position + 1;
			end;
		ensure
			valid_count: count <= array_count;
			widget_added: has (widget);
		end;

	implementation_to_oui (widget_i: WIDGET_I): WIDGET
			-- Object user interface widget associated with current
			-- implementation
		require
			widget_i_exists: widget_i /= Void;
		local
			widget_area: like area;
			i: INTEGER;
			widget: WIDGET
		do
			widget_area := area;
		   	from
				i := 1
			until
				i > count or else Result /= Void
			loop
				widget := widget_area.item (i - 1);
				if widget.implementation = widget_i then
					Result := widget
				end;
				i := i + 1
			end;
			Result := widget
		ensure
			valid_result: Result /= Void;
			valid_implemenation: Result.implementation = widget_i
		end; 

	parent (widget: WIDGET): WIDGET
			-- Parent of `widget'
		require
			widget_exists: widget /= Void
		local
			widget_area: like area;
			i: INTEGER;
			parent_widget: WIDGET;
		do
			if widget.depth > 0 then
				widget_area := area;
				from
					i := index_of (widget) - 1
				until
					Result /= Void
				loop
					parent_widget := widget_area.item (i);
					if parent_widget.depth+1 = widget.depth then
						Result := parent_widget
					end;
					i := i - 1
				end;
			end;
		ensure
			is_root: (Result = Void) implies (widget.depth = 0);
			is_child: (Result /= Void) implies (Result.depth+1 = widget.depth)
		end;

	destroy (widget: WIDGET)
			-- Destroy `widget', i.e. destroy the screen object
			-- and remove it from the list of managed widgets.
			-- Also destroy children (iteratively).
		require
			valid_widget: widget /= Void;
			not_destroyed: not widget.destroyed
		local
			widget_area: like area;
			widget_depth, position: INTEGER;
			nbr_to_remove: INTEGER
			w_position: INTEGER;
			wid: WIDGET;
			stop: BOOLEAN;
			list: LINKED_LIST [WIDGET]
		do
			widget_area := area;
			create list.make;
			list.put_front (widget)
			from
					-- Calculate the number of widgets
					-- to be removed from list.
				w_position := index_of (widget);
				position := w_position + 1;
				nbr_to_remove := 1;
				widget_depth := widget.depth;
			until
				stop or else (position = count) 
			loop
				wid := widget_area.item (position);
				if wid.depth <= widget_depth then
					stop := True
				else
						-- Remove the widget's implementation
					list.put_front (wid);
					check
						wid_not_destroyed: not wid.destroyed
					end;
					position := position + 1;
					nbr_to_remove := nbr_to_remove + 1
				end
			end;
				
					-- Remove widget(s) from Current.
			count := count - nbr_to_remove;
			from
			until
				w_position >= count 
			loop
				wid := widget_area.item (w_position + nbr_to_remove);
				widget_area.put (wid, w_position);
				w_position := w_position + 1;
				wid.implementation.set_widget_index (w_position);
			end;
			from
			until
				nbr_to_remove = 0
			loop
				widget_area.put (Void, nbr_to_remove + count - 1);
				nbr_to_remove := nbr_to_remove - 1
			end;

				-- Correctly destroy the widget's implementation
			widget.implementation.destroy (list);
				-- Remove the widget's implementation
			from
				list.start
			until
				list.after
			loop
				list.item.remove_implementation;
				list.forth
			end
		ensure
			no_void_entries: not has_void_entries 
		end;

	screen (widget: WIDGET): SCREEN
			-- Screen of widget
		require
			widget_exists: widget /= Void;
			has_implementation: not widget.destroyed
		do
			Result := top (widget).screen
		ensure
			valid_result: Result /= Void
		end;

	screen_object_to_oui (screen_object: POINTER): WIDGET
			-- Object user interface widget associated with an
			-- implementation with same `screen_object'
		local
			i: INTEGER;
			widget: WIDGET;
			widget_area: like area;
		do	
			widget_area := area;
			from
				i := 0
			until
				Result /= Void or else i >= count
			loop
				widget := widget_area.item (i);
				if 	
					widget.implementation.screen_object = screen_object 
				then
					Result := widget;
				end;
				i := i+1
			end;
		end;

	show_tree (a_file: PLAIN_TEXT_FILE)
			-- Print a textual representation of the widgets tree on `a_file'.
		require
			a_file_exists: a_file /= Void;
			a_file_opened_for_writing: a_file.is_open_write
		local
			i, j: INTEGER;
			b_routines: BASIC_ROUTINES
		do
			create b_routines;
			from
				i := 1
			until
				i > count 
			loop
				if i_th (i) /= Void then
					from
						j := i_th (i).depth
					until
						j = 0
					loop
						a_file.put_character (b_routines.charconv (Tabulation));
						j := j-1
					end;
					if (i_th (i).identifier = Void) then
						a_file.put_string ("???")
					else
						a_file.put_string (i_th (i).identifier)
					end;
					a_file.new_line
				end;
				i := i+1
			end
		end;

	top (widget: WIDGET): TOP
			-- Top shell or base of the widget
		require
			widget_exists: widget /= Void;
			has_implementation: not widget.destroyed
		local
			widget_area: like area;
			i: INTEGER;
			top_widget: WIDGET;
		do
			widget_area := area;
			from
				i := index_of (widget);
			until
				Result /= Void
			loop
				top_widget := widget_area.item (i);
				if top_widget.depth = 0 then
					Result ?= top_widget
				end;
				i := i - 1
			end;
		ensure
			valid_result: Result /= Void
		end;

	index: INTEGER;
			-- Current cursor index

feature {COMPOSITE} -- Basic operations

	children_of (w: WIDGET): ARRAYED_LIST [WIDGET]
			-- Children of widget `w'
		require
			valid_w: w /= Void;
			w_not_destroyed: not w.destroyed
		local
			position, wc: INTEGER;
			widget: WIDGET;
			wd, current_depth: INTEGER;
			finished: BOOLEAN;
			widget_area: like area
		do
			widget_area := area;
			create Result.make (10);
			wc := count;
			position := index_of (w);
			current_depth := w.depth;
			from
				position := position + 1;
			until
				position = wc or else finished
			loop
				widget := widget_area.item (position);
				wd := widget.depth;
				if wd = current_depth + 1 then
					Result.extend (widget)
				elseif wd <= current_depth then
					finished := True
				end;
				position := position + 1
			end
		ensure
			valid_result: Result /= Void
		end;

	descendants_of (w: WIDGET; desc: ARRAYED_LIST [WIDGET])
			-- Add all descendant children of widget `w' into
			-- `desc'. 
		require
			valid_w: w /= Void;
			valid_desc: desc /= Void
		local
			position, wc: INTEGER;
			current_depth: INTEGER;
			finished: BOOLEAN;
			widget: WIDGET;
			widget_area: like area
		do
			widget_area := area;
			wc := count;
			position := index_of (w);
			current_depth := w.depth;
			from
				position := position + 1;
			until
				position = wc or else finished
			loop
				widget := widget_area.item (position);
				if widget.depth <= current_depth then
					finished := True
				else
					desc.extend (widget);
				end;
				position := position + 1
			end
		end;

feature {G_ANY_I} -- Basic operations

	widget_at (i: INTEGER): WIDGET
			-- Widget at index position `i'.
		require
			valid_index: valid_index (i);
		do
			Result := area.item (i - 1)
		ensure
			valid_result: Result /= Void
		end;

	screen_i_using_index (widget_index: INTEGER): SCREEN_I
			-- Top shell or base of the widget
		require
			valid_index: valid_index (widget_index);
		local
			widget_area: like area;
			i: INTEGER;
			top_widget: WIDGET;
		do
			widget_area := area;
			from
				i := widget_index - 1;
			until
				Result /= Void
			loop
				top_widget := widget_area.item (i);
				if top_widget.depth = 0 then
					Result := top_widget.screen.implementation
				end;
				i := i - 1
			end;
		ensure
			valid_result: Result /= Void
		end;

	parent_using_index (widget: WIDGET; w_index: INTEGER): WIDGET
			-- Parent of `widget'. Start at `w_index'.
		require
			widget_exists: widget /= Void;
			valid_widget_index: valid_index (w_index)
		local
			widget_area: like area;
			i: INTEGER;
			parent_widget: WIDGET;
		do
			if widget.depth > 0 then
				widget_area := area;
				from
					i := w_index - 1
				until
					Result /= Void
				loop
					parent_widget := widget_area.item (i);
					if parent_widget.depth+1 = widget.depth then
						Result := parent_widget
					end;
					i := i - 1
				end;
			end;
		ensure
			is_root: (Result = Void) implies (widget.depth = 0);
			is_child: (Result /= Void) implies (Result.depth+1 = widget.depth)
		end;

feature {NONE} -- Implementation

	Chunk: INTEGER = 50;
			-- Array chunk

	empty: BOOLEAN
			-- Is the list empty ?
		do
			Result := count = 0
		end;

	index_of (widget: WIDGET): INTEGER
			-- Index of `widget' in list
		require
			widget_exists: widget /= Void;
		local
			widget_area: like area;
			widget_i: WIDGET_I
		do
			widget_i := widget.implementation;
			if widget_i /= Void then
				Result := widget_i.widget_index;
			end;
			if Result = 0 then
				widget_area := area;
				from
				until
					widget.same (widget_area.item (Result))
				loop
					Result := Result + 1
				end;
			else
				Result := Result - 1;
			end
		ensure
			Widget_found: widget.same (area.item (Result))
		end;

	has_void_entries: BOOLEAN
			-- Are there void entries in the array?
		do
			from	
				start
			until	
				after or else Result
			loop
				Result := item = Void or else item.implementation = Void
				forth
			end
		end;

invariant

	Count_equal_or_less_list_count: count <= array_count;
	Non_negative_count: count >= 0;
	Non_negative_position: index >= 0;
	Stay_on: index <= count+1;
	Empty_implies_zero_position: empty implies (index = 0)

note
	copyright:	"Copyright (c) 1984-2006, Eiffel Software and others"
	license:	"Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
	source: "[
			 Eiffel Software
			 356 Storke Road, Goleta, CA 93117 USA
			 Telephone 805-685-1006, Fax 805-685-6869
			 Website http://www.eiffel.com
			 Customer support http://support.eiffel.com
		]"




end -- class W_MANAGER