note description: "Scrollable lists" legal: "See notice at end of class." status: "See notice at end of class." date: "$Date$" revision: "$Revision$" class SCROLLABLE_LIST inherit FONTABLE rename implementation as font_implementation end; PRIMITIVE rename cursor as screen_cursor redefine implementation, is_fontable end; create make, make_unmanaged, make_fixed_size, make_fixed_size_unmanaged feature {NONE} -- Initialization make (a_name: STRING; a_parent: COMPOSITE) -- Create a scrolled list with `a_name' as identifier, -- `a_parent' as parent and call `set_default'. -- Scroll list will attempt to resize if entries -- are added. require valid_name: a_name /= Void; valid_parent: a_parent /= Void do create_ev_widget (a_name, a_parent, True, False) ensure parent_set: parent = a_parent; identifier_set: identifier.is_equal (a_name); managed: managed end; make_fixed_size (a_name: STRING; a_parent: COMPOSITE) -- Create a scrolled list with `a_name' as identifier, -- `a_parent' as parent and call `set_default'. -- Scroll list will not resize if entries -- are added. require valid_name: a_name /= Void; valid_parent: a_parent /= Void do create_ev_widget (a_name, a_parent, True, True) ensure parent_set: parent = a_parent; identifier_set: identifier.is_equal (a_name); managed: managed end; make_unmanaged (a_name: STRING; a_parent: COMPOSITE) -- Create an unmanaged scrolled list with `a_name' as identifier, -- `a_parent' as parent and call `set_default'. -- Scroll list will attempt to resize if entries -- are added. require valid_name: a_name /= Void; valid_parent: a_parent /= Void do create_ev_widget (a_name, a_parent, False, False) ensure parent_set: parent = a_parent; identifier_set: identifier.is_equal (a_name); not_managed: not managed end; make_fixed_size_unmanaged (a_name: STRING; a_parent: COMPOSITE) -- Create an unmanaged scrolled list with `a_name' as identifier, -- `a_parent' as parent and call `set_default'. -- Scroll list will not resize if entries -- are added. require valid_name: a_name /= Void; valid_parent: a_parent /= Void do create_ev_widget (a_name, a_parent, False, True) ensure parent_set: parent = a_parent; identifier_set: identifier.is_equal (a_name); not_managed: not managed end; create_ev_widget (a_name: STRING; a_parent: COMPOSITE; man: BOOLEAN; is_fixed: BOOLEAN) -- Create a scrolled list with `a_name' as identifier, -- `a_parent' as parent and call `set_default'. do depth := a_parent.depth+1; widget_manager.new (Current, a_parent); if a_name /= Void then identifier := a_name.twin else identifier := Void end create {SCROLLABLE_LIST_IMP} implementation.make (Current, man, is_fixed, a_parent); implementation.set_widget_default; end; feature -- Access list: LIST [SCROLLABLE_LIST_ELEMENT] -- Duplicate list of all the items local pos: INTEGER; a_list: ARRAYED_LIST [SCROLLABLE_LIST_ELEMENT] do a_list := implementation; pos := a_list.index; a_list.start; Result := a_list.duplicate (a_list.count); a_list.go_i_th (pos) end cursor: CURSOR -- Current cursor position do Result := implementation.cursor end first: like item -- Item at first position require not_empty: not is_empty do Result := implementation.first end i_th, infix "@" (i: INTEGER): like item -- Item at i-th position require valid_key: valid_index (i) do Result := implementation.i_th (i) end index: INTEGER -- Current cursor index do Result := implementation.index end index_of (v: like item i: INTEGER): INTEGER -- Index of i-th occurrence of item identical to v. -- (Reference or object equality, -- based on object_comparison.) -- 0 if none. require positive_occurrences: i > 0 do Result := implementation.index_of (v, i) ensure non_negative_result: Result >= 0 end item: SCROLLABLE_LIST_ELEMENT -- Item at current position require not_off: not off readable: readable do Result ?= implementation.item end last: like item -- Item at last position require not_empty: not is_empty do Result := implementation.last end occurrences (v: like item): INTEGER -- Number of times v appears. -- (Reference or object equality, -- based on object_comparison.) do Result := implementation.occurrences (v) ensure non_negative_occurrences: Result >= 0 end feature -- Status report has (v: like item): BOOLEAN -- Does chain include v? -- (Reference or object equality, -- based on object_comparison.) do Result := implementation.has (v) ensure not_found_in_empty: Result implies not is_empty end feature -- Measurement count: INTEGER -- Number of items do Result := implementation.count end feature -- Conversion linear_representation: LINEAR [SCROLLABLE_LIST_ELEMENT] -- Representation as a linear structure do Result := implementation.linear_representation end feature -- Cursor movement back -- Move to previous position. require not_before: not before do implementation.back ensure moved_back: index = old index - 1 end finish -- Move cursor to last position. -- (No effect if is_empty) do implementation.finish ensure at_last: not is_empty implies islast end forth -- Move to next position if no next position, -- ensure that exhausted will be true. require not_after: not after do implementation.forth ensure moved_forth: index = old index + 1 end go_i_th (i: INTEGER) -- Move cursor to i-th position. require valid_cursor_index: valid_cursor_index (i) do implementation.go_i_th (i) ensure position_expected: index = i end go_to (p: CURSOR) -- Move cursor to position p. require cursor_position_valid: valid_cursor (p) do implementation.go_to (p) end move (i: INTEGER) -- Move cursor i positions. The cursor -- may end up off if the absolute value of i -- is too big. do implementation.move (i) ensure too_far_right: (old index + i > count) implies exhausted too_far_left: (old index + i < 1) implies exhausted expected_index: (not exhausted) implies (index = old index + i) end search (v: like item) -- Move to first position (at or after current -- position) where item and v are equal. -- If structure does not include v ensure that -- exhausted will be true. -- (Reference or object equality, -- based on object_comparison.) do implementation.search (v) ensure object_found: (not exhausted and then object_comparison and then v /= void and then item /= void) implies v.is_equal (item) item_found: (not exhausted and not object_comparison) implies v = item end start -- Move cursor to first position. -- (No effect if is_empty) do implementation.start ensure at_first: not is_empty implies isfirst end feature -- Element change append (s: SEQUENCE [SCROLLABLE_LIST_ELEMENT]) -- Append a copy of s. require argument_not_void: s /= void do implementation.append (s) ensure new_count: count >= old count end extend (v: SCROLLABLE_LIST_ELEMENT) -- Add a new occurrence of v. require extendible: extendible do implementation.extend (v) ensure one_more_occurrence: occurrences (v) = old (occurrences (v)) + 1 item_inserted: has (v) end fill (other: CONTAINER [SCROLLABLE_LIST_ELEMENT]) -- Fill with as many items of other as possible. -- The representations of other and current structure -- need not be the same. require other_not_void: other /= void extendible do implementation.fill (other) end force (v: like item) -- Add v to end. require extendible: extendible do implementation.force (v) ensure new_count: count = old count + 1 item_inserted: has (v) end merge_left (other: ARRAYED_LIST [SCROLLABLE_LIST_ELEMENT]) -- Merge other into current structure before cursor -- position. Do not move cursor. Empty other. require extendible: extendible not_before: not before other_exists: other /= void do implementation.merge_left (other) ensure new_count: count = old count + old other.count new_index: index = old index + old other.count other_is_empty: other.is_empty end merge_right (other: ARRAYED_LIST [SCROLLABLE_LIST_ELEMENT]) -- Merge other into current structure after cursor -- position. Do not move cursor. Empty other. require extendible: extendible not_after: not after other_exists: other /= void do implementation.merge_right (other) ensure new_count: count = old count + old other.count same_index: index = old index other_is_empty: other.is_empty end put (v: like item) -- Replace current item by v. -- (Synonym for replace) require extendible: extendible do implementation.put (v) ensure same_count: count = old count item_inserted: has (v) end put_front (v: like item) -- Add v at beginning. -- Do not move cursor. do implementation.put_front (v) ensure new_count: count = old count + 1 item_inserted: first = v end put_i_th (v: like item i: INTEGER) -- Put v at i-th position. require valid_key: valid_index (i) do implementation.put_i_th (v,i) ensure insertion_done: i_th (i) = v end put_left (v: like item) -- Add v to the left of cursor position. -- Do not move cursor. require extendible: extendible not_before: not before do implementation.put_left (v) ensure new_count: count = old count + 1 new_index: index = old index + 1 end put_right (v: like item) -- Add v to the right of cursor position. -- Do not move cursor. require extendible: extendible not_after: not after do implementation.put_right (v) ensure new_count: count = old count + 1 same_index: index = old index end replace (v: SCROLLABLE_LIST_ELEMENT) -- Replace current item by v. require writable: writable do implementation.replace (v) ensure item_replaced: item = v end feature -- Removal prune (v: like item) -- Remove first occurrence of v, if any, -- after cursor position. -- If found, move cursor to right neighbor -- if not, make structure exhausted. require prunable: prunable do implementation.prune (v) end prune_all (v: like item) -- Remove all occurrences of v. -- (Reference or object equality, -- based on object_comparison.) -- Leave structure exhausted. require prunable do implementation.prune_all (v) ensure is_exhausted: exhausted no_more_occurrences: not has (v) end remove -- Remove current item. -- Move cursor to right neighbor -- (or after if no right neighbor). require prunable: prunable writable: writable do implementation.remove ensure after_when_empty: is_empty implies after end remove_left -- Remove item to the left of cursor position. -- Do not move cursor. require not_before: not before left_exists: index > 1 do implementation.remove_left ensure new_count: count = old count - 1 new_index: index = old index - 1 end remove_right -- Remove item to the right of cursor position. -- Do not move cursor. require right_exists: index < count do implementation.remove_right ensure new_count: count = old count - 1 same_index: index = old index end wipe_out -- Remove all items. require prunable: prunable do implementation.wipe_out ensure is_before: before wiped_out: is_empty end remove_click_action, remove_selection_action (a_command: COMMAND; argument: ANY) -- Remove `a_command' to the list of action to execute when items are -- selected with click selection mode in current scroll list. require exists: not destroyed; not_a_command_void: a_command /= Void do implementation.remove_click_action (a_command, argument) end; feature -- Status report after: BOOLEAN -- Is there no valid cursor position to the right of cursor? do Result := implementation.after end before: BOOLEAN -- Is there no valid cursor position to the left of cursor? do Result := implementation.before end changeable_comparison_criterion: BOOLEAN -- May object_comparison be changed? -- (Answer: yes by default.) do Result := implementation.changeable_comparison_criterion end is_empty: BOOLEAN -- Is structure empty? do Result := implementation.is_empty end empty: BOOLEAN -- Is structure empty? obsolete "Use `is_empty' instead" do Result := is_empty end exhausted: BOOLEAN -- Has structure been completely explored? do Result := implementation.exhausted ensure exhausted_when_off: off implies Result end extendible: BOOLEAN -- May new items be added? do Result := implementation.extendible end full: BOOLEAN -- Is structure filled to capacity? do Result := implementation.full end isfirst: BOOLEAN -- Is cursor at first position? do Result := implementation.isfirst ensure valid_position: Result implies not is_empty end islast: BOOLEAN -- Is cursor at last position? do Result := implementation.islast ensure valid_position: Result implies not is_empty end object_comparison: BOOLEAN -- Must search operations use equal rather than = -- for comparing references? (Default: no, use =.) do Result := implementation.object_comparison end off: BOOLEAN -- Is there no current item? do Result := implementation.off end prunable: BOOLEAN -- May items be removed? (Answer: yes.) do Result := implementation.prunable end readable: BOOLEAN -- Is there a current item that may be read? do Result := implementation.readable end selected_count: INTEGER -- Number of selected items in current list require exists: not destroyed; do Result := implementation.selected_count end; selected_item: SCROLLABLE_LIST_ELEMENT -- Selected item if single or browse selection mode is selected -- Void if nothing is selected require exists: not destroyed; do Result := implementation.selected_item end; selected_items: LINKED_LIST [SCROLLABLE_LIST_ELEMENT] -- Selected items require exists: not destroyed; do Result := implementation.selected_items end; selected_position: INTEGER -- Position of selected item if single or browse selection mode is -- selected -- 0 if nothing is selected require exists: not destroyed; do Result := implementation.selected_position end; selected_positions: LINKED_LIST [INTEGER] -- Positions of the selected items require exists: not destroyed; do Result := implementation.selected_positions end; valid_cursor (p: CURSOR): BOOLEAN -- Can the cursor be moved to position p? do Result := implementation.valid_cursor (p) end valid_cursor_index (i: INTEGER): BOOLEAN -- Is i correctly bounded for cursor movement? do Result := implementation.valid_cursor_index (i) ensure valid_cursor_index_definition: Result = ((i >= 0) and (i <= count + 1)) end valid_index (i: INTEGER): BOOLEAN -- Is i within allowable bounds? do Result := implementation.valid_index (i) ensure valid_index_definition: Result = (i >= 1) and (i <= count) end visible_item_count: INTEGER -- Number of visible item of list do result := implementation.visible_item_count end; writable: BOOLEAN -- Is there a current item that may be modified? do Result := implementation.writable end feature -- Status setting compare_objects -- Ensure that future search operations will use equal -- rather than = for comparing references. require changeable_comparison_criterion do implementation.compare_objects ensure object_comparison: object_comparison end compare_references -- Ensure that future search operations will use = -- rather than equal for comparing references. require changeable_comparison_criterion do implementation.compare_references ensure reference_comparison: not object_comparison end deselect_all -- Deselect all selected items. require exists: not destroyed; do implementation.deselect_all ensure selected_list_is_empty: selected_count = 0 end; scroll_to_current -- Make `item' the first visible item in the list if -- `position' < `first_visible_item_position'. -- Make `item' the last visible item in the list if -- `position' >= `first_visible_item_position'+`visible_item_count'. -- Do nothing if `item' is visible. require exists: not destroyed; not_off: not off do implementation.scroll_to_current end; select_item -- Select item at current position. require exists: not destroyed; not_off: not off do implementation.select_item end; deselect_item -- Deselect item at current position. require exists: not destroyed; not_off: not off do implementation.deselect_item end; select_i_th (i: INTEGER) -- Select item at `i'-th position. require exists: not destroyed; index_large_enough: i >= 1; index_small_enough: i <= count do implementation.select_i_th (i) end; deselect_i_th (i: INTEGER) -- Deselect item at `i'-th position. require exists: not destroyed; index_large_enough: i >= 1; index_small_enough: i <= count do implementation.deselect_i_th (i) end; set_multiple_selection -- Set the selection to be multiple items require exists: not destroyed; not_realized: not realized or else not shown do implementation.set_multiple_selection end set_single_selection -- Set the selection to be single items require exists: not destroyed; not_realized: not realized or else not shown do implementation.set_single_selection end set_visible_item_count (a_count: INTEGER) -- Set the number of visible items to `a_count'. require exists: not destroyed; a_count_large_enough: a_count > 0 do implementation.set_visible_item_count (a_count) end; feature -- Element change add_click_action, add_selection_action (a_command: COMMAND; argument: ANY) -- Add `a_command' to the list of actions to execute when items are -- selected with click selection mode in current scroll list. require exists: not destroyed; not_a_command_void: a_command /= Void do implementation.add_click_action (a_command, argument) end; feature -- Default Action commands add_default_action (a_command: COMMAND; argument: ANY) -- Add `a_command' to the list of actions to -- execute when items are selected with double -- click or by pressing `RETURN' in current -- scroll list. require exists: not destroyed; not_a_command_void: a_command /= Void do implementation.add_default_action (a_command, argument) end; remove_default_action -- Remove all actions executed when items are -- selected with double click or by pressing -- `RETURN' in current scroll list. require exists: not destroyed; do implementation.remove_default_action end; feature -- Transformation swap (i: INTEGER) -- Exchange item at i-th position with item -- at cursor position. require not_off: not off valid_index: valid_index (i) do implementation.swap (i) ensure swapped_to_item: item = old i_th (i) swapped_from_item: i_th (i) = old item end feature {G_ANY, G_ANY_I, WIDGET_I, TOOLKIT} -- Implementation implementation: SCROLLABLE_LIST_I; -- Implementation of list feature {G_ANY, G_ANY_I, WIDGET_I} -- Implementation is_fontable: BOOLEAN = true; -- Is current widget an heir of FONTABLE? set_default do end invariant before_definition: not destroyed implies (before = (index = 0)) after_definition: not destroyed implies (after = (index = count + 1)) non_negative_index: not destroyed implies (index >= 0) index_small_enough: not destroyed implies (index <= count + 1) off_definition: not destroyed implies (off = ((index = 0) or (index = count + 1))) isfirst_definition: not destroyed implies (isfirst = ((not is_empty) and (index = 1))) islast_definition: not destroyed implies (islast = ((not is_empty) and (index = count))) item_corresponds_to_index: not destroyed implies ((not off) implies (item = i_th (index))) writable_constraint: not destroyed implies (writable implies readable) empty_constraint: not destroyed implies (is_empty implies (not readable) and (not writable)) not_both: not destroyed implies (not (after and before)) empty_property: not destroyed implies (is_empty implies (after or before)) before_constraint: not destroyed implies (before implies off) after_constraint: not destroyed implies (after implies off) empty_constraint: not destroyed implies (is_empty implies off) empty_definition: not destroyed implies (is_empty = (count = 0)) non_negative_count: not destroyed implies (count >= 0) extendible: not destroyed implies extendible 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 SCROLLABLE_LIST