note description: "A sequence of actions to be performed on call." legal: "See notice at end of class." instructions: "[ Use features inherited from LIST to add/remove actions. An action is a procedure of ANY class that takes EVENT_DATA. When call is called the actions in the list will be executed in order stating at first. An action may call abort which will cause call to stop executing actions in the sequence. (Until the next call to call). Descendants may redefine initialize to arrange for call to be called by an event source. Use block, pause, flush and resume to change the behavior of call. eg. birthday_data: TUPLE [INTEGER, STRING] -- (age, name) birthday_actions: ACTION_SEQUENCE [like birthday_data] create birthday_actions.make ("birthday", <<"age","name">>) send_card (age: INTEGER, name, from: STRING) is ... buy_gift (age: INTEGER, name, gift, from: STRING) is ... birthday_actions.extend (agent send_card (?, ?, "Sam") birthday_actions.extend (agent buy_gift (?, ?, "Wine", "Sam") birthday_actions.call ([35, "Julia"]) causes call to: send_card (35, "Julia", "Sam") buy_gift (35, "Julia", "Wine", "Sam") ]" status: "See notice at end of class." keywords: event, action date: "$Date: 2018-11-14 15:15:17 +0000 (Wed, 14 Nov 2018) $" revision: "$Revision: 102463 $" class interface ACTION_SEQUENCE [EVENT_DATA -> detachable TUPLE create default_create end] create default_create -- Begin in Normal_state. require -- from ANY True make create {ACTION_SEQUENCE} arrayed_list_make (n: INTEGER_32) -- Allocate list with n items. -- (n may be zero for empty list.) -- (from ARRAYED_LIST) require -- from ARRAYED_LIST valid_number_of_items: n >= 0 ensure -- from ARRAYED_LIST correct_position: before is_empty: is_empty make_filled (n: INTEGER_32) -- Allocate list with n items. -- (n may be zero for empty list.) -- This list will be full. -- (from ARRAYED_LIST) require -- from ARRAYED_LIST valid_number_of_items: n >= 0 has_default: ({PROCEDURE [EVENT_DATA]}).has_default ensure -- from ARRAYED_LIST correct_position: before filled: full feature -- Initialization arrayed_list_make (n: INTEGER_32) -- Allocate list with n items. -- (n may be zero for empty list.) -- (from ARRAYED_LIST) require -- from ARRAYED_LIST valid_number_of_items: n >= 0 ensure -- from ARRAYED_LIST correct_position: before is_empty: is_empty make_filled (n: INTEGER_32) -- Allocate list with n items. -- (n may be zero for empty list.) -- This list will be full. -- (from ARRAYED_LIST) require -- from ARRAYED_LIST valid_number_of_items: n >= 0 has_default: ({PROCEDURE [EVENT_DATA]}).has_default ensure -- from ARRAYED_LIST correct_position: before filled: full feature -- Access area: SPECIAL [PROCEDURE [EVENT_DATA]] -- Access to internal storage of ARRAYED_LIST -- (from ARRAYED_LIST) area_v2: SPECIAL [PROCEDURE [EVENT_DATA]] -- Special data zone. -- (from TO_SPECIAL) at alias "@" (i: INTEGER_32): like item assign put_i_th -- Item at i-th position -- Was declared in ARRAYED_LIST as synonym of i_th. -- (from ARRAYED_LIST) require -- from TABLE valid_key: valid_index (i) array_at (i: INTEGER_32): PROCEDURE [EVENT_DATA] assign array_put -- Entry at index i, if in index interval. -- Was declared in TO_SPECIAL as synonym of item. -- (from TO_SPECIAL) require -- from TO_SPECIAL valid_index: array_valid_index (i) cursor: ARRAYED_LIST_CURSOR -- Current cursor position -- (from ARRAYED_LIST) ensure -- from CURSOR_STRUCTURE cursor_not_void: Result /= Void first: like item -- Item at first position -- (from ARRAYED_LIST) require -- from CHAIN not_empty: not is_empty generating_type: TYPE [detachable ACTION_SEQUENCE [EVENT_DATA]] -- Type of current object -- (type of which it is a direct instance) -- (from ANY) ensure -- from ANY generating_type_not_void: Result /= Void generator: STRING_8 -- Name of current object's generating class -- (base class of the type of which it is a direct instance) -- (from ANY) ensure -- from ANY generator_not_void: Result /= Void generator_not_empty: not Result.is_empty has (v: like item): BOOLEAN -- Does current include v? -- (Reference or object equality, -- based on object_comparison.) -- (from ARRAYED_LIST) require -- from CONTAINER True ensure -- from CONTAINER not_found_in_empty: Result implies not is_empty sequential_has (v: like item): BOOLEAN -- Does structure include an occurrence of v? -- (Reference or object equality, -- based on object_comparison.) -- (from LINEAR) require -- from CONTAINER True ensure -- from CONTAINER not_found_in_empty: Result implies not is_empty i_th alias "[]" (i: INTEGER_32): like item assign put_i_th -- Item at i-th position -- Was declared in ARRAYED_LIST as synonym of at. -- (from ARRAYED_LIST) require -- from TABLE valid_key: valid_index (i) require -- from READABLE_INDEXABLE valid_index: valid_index (i) index: INTEGER_32 -- Index of item, if valid. -- (from ARRAYED_LIST) index_of (v: like item; i: INTEGER_32): INTEGER_32 -- Index of i-th occurrence of item identical to v. -- (Reference or object equality, -- based on object_comparison.) -- 0 if none. -- (from CHAIN) sequential_index_of (v: like item; i: INTEGER_32): INTEGER_32 -- Index of i-th occurrence of v. -- 0 if none. -- (Reference or object equality, -- based on object_comparison.) -- (from LINEAR) require -- from LINEAR positive_occurrences: i > 0 ensure -- from LINEAR non_negative_result: Result >= 0 item: PROCEDURE [EVENT_DATA] -- Current item -- (from ARRAYED_LIST) require -- from ACTIVE readable: readable require -- from TRAVERSABLE not_off: not off require else -- from ARRAYED_LIST index_is_valid: valid_index (index) array_item (i: INTEGER_32): PROCEDURE [EVENT_DATA] assign array_put -- Entry at index i, if in index interval. -- Was declared in TO_SPECIAL as synonym of at. -- (from TO_SPECIAL) require -- from TO_SPECIAL valid_index: array_valid_index (i) item_for_iteration: PROCEDURE [EVENT_DATA] -- Item at current position -- (from LINEAR) require -- from LINEAR not_off: not off last: like first -- Item at last position -- (from ARRAYED_LIST) require -- from CHAIN not_empty: not is_empty name: detachable STRING_8 -- Textual description. ensure equal_to_name_internal: Result ~ name_internal new_cursor: ARRAYED_LIST_ITERATION_CURSOR [PROCEDURE [EVENT_DATA]] -- Fresh cursor associated with current structure -- (from ARRAYED_LIST) require -- from ITERABLE True ensure -- from ITERABLE result_attached: Result /= Void sequential_occurrences (v: like item): INTEGER_32 -- Number of times v appears. -- (Reference or object equality, -- based on object_comparison.) -- (from LINEAR) require -- from BAG True ensure -- from BAG non_negative_occurrences: Result >= 0 to_array: ARRAY [PROCEDURE [EVENT_DATA]] -- Share content to be used as an ARRAY. -- Note that although the content is shared, it might -- not be shared when a resizing occur in either ARRAY or Current. -- (from ARRAYED_LIST) ensure -- from ARRAYED_LIST to_array_attached: Result /= Void array_lower_set: Result.lower = 1 array_upper_set: Result.upper = count shared_area: Result.area = area feature -- Measurement additional_space: INTEGER_32 -- Proposed number of additional items -- (from RESIZABLE) ensure -- from RESIZABLE at_least_one: Result >= 1 capacity: INTEGER_32 -- Number of items that may be stored -- (from ARRAYED_LIST) ensure -- from BOUNDED capacity_non_negative: Result >= 0 count: INTEGER_32 -- Number of items. -- (from ARRAYED_LIST) require -- from FINITE True require -- from READABLE_INDEXABLE True ensure -- from FINITE count_non_negative: Result >= 0 Growth_percentage: INTEGER_32 = 50 -- Percentage by which structure will grow automatically -- (from RESIZABLE) Lower: INTEGER_32 = 1 -- Minimum index. -- (from CHAIN) Minimal_increase: INTEGER_32 = 5 -- Minimal number of additional items -- (from RESIZABLE) occurrences (v: like item): INTEGER_32 -- Number of times v appears. -- (Reference or object equality, -- based on object_comparison.) -- (from CHAIN) upper: INTEGER_32 -- Maximum index. -- Use count instead. -- (from ARRAYED_LIST) ensure -- from ARRAYED_LIST definition: Result = count feature -- Comparison frozen deep_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void -- or attached to isomorphic object structures? -- (from ANY) ensure -- from ANY instance_free: class shallow_implies_deep: standard_equal (a, b) implies Result both_or_none_void: (a = Void) implies (Result = (b = Void)) same_type: (Result and (a /= Void)) implies (b /= Void and then a.same_type (b)) symmetric: Result implies deep_equal (b, a) frozen equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached -- to objects considered equal? -- (from ANY) ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.is_equal (b)) frozen is_deep_equal alias "≡≡≡" (other: ACTION_SEQUENCE [EVENT_DATA]): BOOLEAN -- Are Current and other attached to isomorphic object structures? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY shallow_implies_deep: standard_is_equal (other) implies Result same_type: Result implies same_type (other) symmetric: Result implies other.is_deep_equal (Current) is_equal (other: ACTION_SEQUENCE [EVENT_DATA]): BOOLEAN -- Is array made of the same items as other? -- (from ARRAYED_LIST) require -- from ANY other_not_void: other /= Void ensure -- from ANY symmetric: Result implies other ~ Current consistent: standard_is_equal (other) implies Result ensure then -- from LIST indices_unchanged: index = old index and other.index = old other.index true_implies_same_size: Result implies count = other.count frozen standard_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached to -- field-by-field identical objects of the same type? -- Always uses default object comparison criterion. -- (from ANY) ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.standard_is_equal (b)) frozen standard_is_equal alias "≜" (other: ACTION_SEQUENCE [EVENT_DATA]): BOOLEAN -- Is other attached to an object of the same type -- as current object, and field-by-field identical to it? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY same_type: Result implies same_type (other) symmetric: Result implies other.standard_is_equal (Current) feature -- Status report after: BOOLEAN -- Is there no valid cursor position to the right of cursor? -- (from LIST) require -- from LINEAR True all_default: BOOLEAN -- Are all items set to default values? -- (from ARRAYED_LIST) require -- from ARRAYED_LIST has_default: ({PROCEDURE [EVENT_DATA]}).has_default before: BOOLEAN -- Is there no valid cursor position to the left of cursor? -- (from LIST) require -- from BILINEAR True Blocked_state: INTEGER_32 = 3 call_is_underway: BOOLEAN -- Is call currently being executed? ensure Result = not is_aborted_stack.is_empty changeable_comparison_criterion: BOOLEAN -- May object_comparison be changed? -- (Answer: yes by default.) -- (from CONTAINER) conforms_to (other: ANY): BOOLEAN -- Does type of current object conform to type -- of other (as per Eiffel: The Language, chapter 13)? -- (from ANY) require -- from ANY other_not_void: other /= Void exhausted: BOOLEAN -- Has structure been completely explored? -- (from LINEAR) ensure -- from LINEAR exhausted_when_off: off implies Result extendible: BOOLEAN -- May new items be added? (Answer: yes.) -- (from DYNAMIC_CHAIN) require -- from COLLECTION True full: BOOLEAN -- Is structure full? -- (from BOUNDED) require -- from BOX True is_empty: BOOLEAN -- Is structure empty? -- (from FINITE) is_inserted (v: PROCEDURE [EVENT_DATA]): BOOLEAN -- Has v been inserted at the end by the most recent put or -- extend? -- (from ARRAYED_LIST) isfirst: BOOLEAN -- Is cursor at first position? -- (from CHAIN) ensure -- from CHAIN valid_position: Result implies not is_empty islast: BOOLEAN -- Is cursor at last position? -- (from CHAIN) ensure -- from CHAIN valid_position: Result implies not is_empty Normal_state: INTEGER_32 = 1 object_comparison: BOOLEAN -- Must search operations use equal rather than = -- for comparing references? (Default: no, use =.) -- (from CONTAINER) off: BOOLEAN -- Is there no current item? -- (from CHAIN) require -- from TRAVERSABLE True Paused_state: INTEGER_32 = 2 prunable: BOOLEAN -- May items be removed? (Answer: yes.) -- (from ARRAYED_LIST) require -- from COLLECTION True readable: BOOLEAN -- Is there a current item that may be read? -- (from SEQUENCE) require -- from ACTIVE True replaceable: BOOLEAN -- Can current item be replaced? -- (from ACTIVE) resizable: BOOLEAN -- May capacity be changed? (Answer: yes.) -- (from RESIZABLE) same_type (other: ANY): BOOLEAN -- Is type of current object identical to type of other? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY definition: Result = (conforms_to (other) and other.conforms_to (Current)) state: INTEGER_32 -- One of Normal_state Paused_state or Blocked_state valid_cursor (p: CURSOR): BOOLEAN -- Can the cursor be moved to position p? -- (from ARRAYED_LIST) valid_cursor_index (i: INTEGER_32): BOOLEAN -- Is i correctly bounded for cursor movement? -- (from CHAIN) ensure -- from CHAIN valid_cursor_index_definition: Result = ((i >= 0) and (i <= count + 1)) valid_index (i: INTEGER_32): BOOLEAN -- Is i a valid index? -- (from ARRAYED_LIST) require -- from READABLE_INDEXABLE True require -- from TABLE True ensure -- from READABLE_INDEXABLE only_if_in_index_set: Result implies (Lower <= i and i <= count) ensure then -- from CHAIN valid_index_definition: Result = ((i >= 1) and (i <= count)) array_valid_index (i: INTEGER_32): BOOLEAN -- Is i within the bounds of Current? -- (from TO_SPECIAL) writable: BOOLEAN -- Is there a current item that may be modified? -- (from SEQUENCE) require -- from ACTIVE True feature -- Status setting abort -- Abort the current call. -- (The current item.call will be completed.) require call_is_underway: call_is_underway ensure is_aborted_set: is_aborted_stack.item block -- Ignore subsequent calls. ensure blocked_state: state = Blocked_state compare_objects -- Ensure that future search operations will use equal -- rather than = for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion: changeable_comparison_criterion ensure -- from CONTAINER object_comparison compare_references -- Ensure that future search operations will use = -- rather than equal for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion: changeable_comparison_criterion ensure -- from CONTAINER reference_comparison: not object_comparison flush -- Discard any buffered calls. ensure call_buffer_empty: call_buffer.is_empty pause -- Buffer subsequent calls for later execution. -- If is_blocked calls will simply be ignored. ensure paused_state: state = Paused_state resume -- Used after block or pause to resume normal call -- execution. Executes any buffered calls. ensure normal_state: state = Normal_state feature -- Cursor movement back -- Move cursor one position backward. -- (from ARRAYED_LIST) require -- from BILINEAR not_before: not before finish -- Move cursor to last position if any. -- (from ARRAYED_LIST) require -- from LINEAR True ensure then -- from CHAIN at_last: not is_empty implies islast ensure then -- from ARRAYED_LIST before_when_empty: is_empty implies before forth -- Move cursor one position forward. -- (from ARRAYED_LIST) require -- from LINEAR not_after: not after ensure then -- from LIST moved_forth: index = old index + 1 go_i_th (i: INTEGER_32) -- Move cursor to i-th position. -- (from ARRAYED_LIST) require -- from CHAIN valid_cursor_index: valid_cursor_index (i) ensure -- from CHAIN position_expected: index = i go_to (p: CURSOR) -- Move cursor to position p. -- (from ARRAYED_LIST) require -- from CURSOR_STRUCTURE cursor_position_valid: valid_cursor (p) move (i: INTEGER_32) -- Move cursor i positions. -- (from ARRAYED_LIST) ensure -- from CHAIN 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) 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.) -- (from ARRAYED_LIST) require -- from LINEAR True ensure -- from LINEAR object_found: (not exhausted and object_comparison) implies v ~ item item_found: (not exhausted and not object_comparison) implies v = item start -- Move cursor to first position if any. -- (from ARRAYED_LIST) require -- from TRAVERSABLE True ensure then -- from CHAIN at_first: not is_empty implies isfirst ensure then -- from ARRAYED_LIST after_when_empty: is_empty implies after feature -- Element change fill (other: CONTAINER [PROCEDURE [EVENT_DATA]]) -- Fill with as many items of other as possible. -- The representations of other and current structure -- need not be the same. -- (from CHAIN) require -- from COLLECTION other_not_void: other /= Void extendible: extendible force (v: like item) -- Add v to end. -- Do not move cursor. -- Was declared in ARRAYED_LIST as synonym of extend. -- (from ARRAYED_LIST) require -- from SEQUENCE extendible: extendible ensure then -- from SEQUENCE new_count: count = old count + 1 item_inserted: has (v) array_put (v: PROCEDURE [EVENT_DATA]; i: INTEGER_32) -- Replace i-th entry, if in index interval, by v. -- (from TO_SPECIAL) require -- from TO_SPECIAL valid_index: array_valid_index (i) ensure -- from TO_SPECIAL inserted: array_item (i) = v put (v: like item) -- Replace current item by v. -- (Synonym for replace) -- (from CHAIN) require -- from CHAIN writeable: writable replaceable: replaceable ensure -- from CHAIN same_count: count = old count is_inserted: is_inserted (v) sequence_put (v: like item) -- Add v to end. -- (from SEQUENCE) require -- from COLLECTION extendible: extendible ensure -- from COLLECTION item_inserted: is_inserted (v) ensure then -- from SEQUENCE new_count: count = old count + 1 feature -- Removal prune (v: like item) -- Remove first occurrence of v, if any, -- after cursor position. -- Move cursor to right neighbor. -- (or after if no right neighbor or v does not occur) require -- from COLLECTION prunable: prunable prune_when_called (an_action: like item) -- Remove an_action after the next time it is called. require has (an_action) remove_i_th (i: INTEGER_32) -- Remove item at index i. -- Move cursor to next neighbor (or after if no next neighbor) if it is at i-th position. -- Do not change cursor otherwise. -- (from ARRAYED_LIST) require -- from DYNAMIC_TABLE prunable: prunable valid_key: valid_index (i) ensure then -- from DYNAMIC_CHAIN new_count: count = old count - 1 same_index_if_below: index <= i implies index = old index new_index_if_above: index > i implies index = old index - 1 same_leading_items: across old twin as c all c.target_index < i implies c.item = i_th (c.target_index) end same_trailing_items: across old twin as c all c.target_index > i implies c.item = i_th (c.target_index - 1) end remove_left -- Remove item to the left of cursor position. -- Do not move cursor. -- (from ARRAYED_LIST) require -- from DYNAMIC_CHAIN left_exists: index > 1 ensure -- from DYNAMIC_CHAIN new_count: count = old count - 1 new_index: index = old index - 1 wipe_out -- Remove all items. -- (from INTERACTIVE_LIST) ensure then -- from DYNAMIC_LIST is_before: before chain_wipe_out -- Remove all items. -- (from DYNAMIC_CHAIN) require -- from COLLECTION prunable: prunable ensure -- from COLLECTION wiped_out: is_empty feature -- Resizing automatic_grow -- Change the capacity to accommodate at least -- Growth_percentage more items. -- (from RESIZABLE) require -- from RESIZABLE resizable: resizable ensure -- from RESIZABLE increased_capacity: capacity >= old capacity + old additional_space grow (i: INTEGER_32) -- Change the capacity to at least i. -- (from ARRAYED_LIST) require -- from RESIZABLE resizable: resizable ensure -- from RESIZABLE new_capacity: capacity >= i resize (new_capacity: INTEGER_32) -- Resize list so that it can contain -- at least n items. Do not lose any item. -- (from ARRAYED_LIST) require -- from ARRAYED_LIST resizable: resizable new_capacity_large_enough: new_capacity >= capacity ensure -- from ARRAYED_LIST capacity_set: capacity >= new_capacity trim -- Decrease capacity to the minimum value. -- Apply to reduce allocated storage. -- (from ARRAYED_LIST) require -- from RESIZABLE True ensure -- from RESIZABLE same_count: count = old count minimal_capacity: capacity = count ensure then -- from ARRAYED_LIST same_items: to_array.same_items (old to_array) feature -- Transformation swap (i: INTEGER_32) -- Exchange item at i-th position with item -- at cursor position. -- (from ARRAYED_LIST) require -- from CHAIN not_off: not off valid_index: valid_index (i) ensure -- from CHAIN swapped_to_item: item = old i_th (i) swapped_from_item: i_th (i) = old item feature -- Conversion linear_representation: LINEAR [PROCEDURE [EVENT_DATA]] -- Representation as a linear structure -- (from LINEAR) require -- from CONTAINER True feature -- Duplication copy (other: ACTION_SEQUENCE [EVENT_DATA]) -- Reinitialize by copying all the items of other. -- (This is also used by clone.) -- (from ARRAYED_LIST) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) ensure -- from ANY is_equal: Current ~ other ensure then -- from ARRAYED_LIST equal_areas: area_v2 ~ other.area_v2 frozen deep_copy (other: ACTION_SEQUENCE [EVENT_DATA]) -- Effect equivalent to that of: -- copy (other . deep_twin) -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY deep_equal: deep_equal (Current, other) frozen deep_twin: ACTION_SEQUENCE [EVENT_DATA] -- New object structure recursively duplicated from Current. -- (from ANY) ensure -- from ANY deep_twin_not_void: Result /= Void deep_equal: deep_equal (Current, Result) frozen standard_copy (other: ACTION_SEQUENCE [EVENT_DATA]) -- Copy every field of other onto corresponding field -- of current object. -- (from ANY) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) ensure -- from ANY is_standard_equal: standard_is_equal (other) frozen standard_twin: ACTION_SEQUENCE [EVENT_DATA] -- New object field-by-field identical to other. -- Always uses default copying semantics. -- (from ANY) ensure -- from ANY standard_twin_not_void: Result /= Void equal: standard_equal (Result, Current) frozen twin: ACTION_SEQUENCE [EVENT_DATA] -- New object equal to Current -- twin calls copy; to change copying/twinning semantics, redefine copy. -- (from ANY) ensure -- from ANY twin_not_void: Result /= Void is_equal: Result ~ Current feature -- Miscellaneous on_item_added_at (an_item: like item; item_index: INTEGER_32) -- an_item has just been added at index item_index. require -- from INTERACTIVE_LIST item_index_valid: (1 <= item_index) and (item_index <= count) on_item_removed_at (an_item: like item; item_index: INTEGER_32) -- an_item has just been removed from index item_index. require -- from INTERACTIVE_LIST item_index_valid: (1 <= item_index) and (item_index <= count + 1) feature -- Basic operations call (event_data: detachable EVENT_DATA) -- Call each procedure in order unless is_blocked. -- If is_paused delay execution until resume. -- Stop at current point in list on abort. ensure is_aborted_stack_unchanged: (old is_aborted_stack) ~ is_aborted_stack frozen default: detachable ACTION_SEQUENCE [EVENT_DATA] -- Default value of object's type -- (from ANY) frozen default_pointer: POINTER -- Default value of type POINTER -- (Avoid the need to write p.default for -- some p of type POINTER.) -- (from ANY) ensure -- from ANY instance_free: class default_rescue -- Process exception for routines with no Rescue clause. -- (Default: do nothing.) -- (from ANY) frozen do_nothing -- Execute a null action. -- (from ANY) ensure -- from ANY instance_free: class extend_kamikaze (an_item: like item) -- Extend an_item and remove it again after it is called. feature -- Correction Mismatch_information: MISMATCH_INFORMATION -- Original attribute values of mismatched object -- (from MISMATCH_CORRECTOR) feature -- Element Change append (s: SEQUENCE [like item]) -- Append a copy of s. -- (from INTERACTIVE_LIST) require -- from SEQUENCE argument_not_void: s /= Void ensure -- from SEQUENCE new_count: count >= old count extend (v: like item) -- Add v to end. -- Do not move cursor. -- (from INTERACTIVE_LIST) require -- from COLLECTION extendible: extendible ensure -- from COLLECTION item_inserted: is_inserted (v) merge_left (other: ACTION_SEQUENCE [EVENT_DATA]) -- Merge other into current structure after cursor -- position. Do not move cursor. Empty other -- (from INTERACTIVE_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_before: not before other_exists: other /= Void not_current: other /= Current ensure -- from DYNAMIC_CHAIN new_count: count = old count + old other.count new_index: index = old index + old other.count other_is_empty: other.is_empty merge_right (other: ACTION_SEQUENCE [EVENT_DATA]) -- Merge other into current structure before cursor -- position. Do not move cursor. Empty other -- (from INTERACTIVE_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_after: not after other_exists: other /= Void not_current: other /= Current ensure -- from DYNAMIC_CHAIN new_count: count = old count + old other.count same_index: index = old index other_is_empty: other.is_empty prune_all (v: like item) -- Remove all occurrences of v. -- (Reference or object equality, -- based on object_comparison.) -- (from INTERACTIVE_LIST) require -- from COLLECTION prunable: prunable ensure -- from COLLECTION no_more_occurrences: not has (v) ensure then -- from DYNAMIC_CHAIN is_exhausted: exhausted ensure then -- from ARRAYED_LIST is_after: after ensure then -- from INTERACTIVE_LIST is_after: after put_front (v: like item) -- Add v to beginning. -- Do not move cursor. -- (from INTERACTIVE_LIST) require -- from DYNAMIC_CHAIN extendible: extendible ensure -- from DYNAMIC_CHAIN new_count: count = old count + 1 item_inserted: first = v put_i_th (v: like i_th; i: INTEGER_32) -- Replace i-th entry, if in index interval, by v. -- (from INTERACTIVE_LIST) require -- from TABLE valid_key: valid_index (i) require -- from TABLE valid_key: valid_index (i) ensure -- from TABLE inserted: i_th (i) = v put_left (v: like item) -- Add v to the left of cursor position. -- Do not move cursor. -- (from INTERACTIVE_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_before: not before ensure -- from DYNAMIC_CHAIN new_count: count = old count + 1 new_index: index = old index + 1 put_right (v: like item) -- Add v to the right of cursor position. -- Do not move cursor. -- (from INTERACTIVE_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_after: not after ensure -- from DYNAMIC_CHAIN new_count: count = old count + 1 same_index: index = old index remove -- Remove current item. -- Move cursor to right neighbor -- (or after if no right neighbor). -- (from INTERACTIVE_LIST) require -- from ACTIVE prunable: prunable writable: writable ensure then -- from DYNAMIC_LIST after_when_empty: is_empty implies after ensure then -- from ARRAYED_LIST index: index = old index remove_right -- Remove item to the right of cursor position. -- Do not move cursor. -- (from INTERACTIVE_LIST) require -- from DYNAMIC_CHAIN right_exists: index < count ensure -- from DYNAMIC_CHAIN new_count: count = old count - 1 same_index: index = old index replace (v: like item) -- Replace current item by v. -- (from INTERACTIVE_LIST) require -- from ACTIVE writable: writable replaceable: replaceable ensure -- from ACTIVE item_replaced: item = v update_for_added (start_index: INTEGER_32) -- Call added_item for all items from index start_index to count -- (from INTERACTIVE_LIST) feature -- Element status has_kamikaze_action (an_action: like item): BOOLEAN -- Return True is an_action is found and will be pruned when called. require has (an_action) feature -- Event handling empty_actions: ARRAYED_LIST [PROCEDURE] -- Actions to be performed on transition from not is_empty to is_empty. not_empty_actions: ARRAYED_LIST [PROCEDURE] -- Actions to be performed on transition from is_empty to not is_empty. feature -- Iteration do_all (action: PROCEDURE [PROCEDURE [EVENT_DATA]]) -- Apply action to every item, from first to last. -- Semantics not guaranteed if action changes the structure; -- in such a case, apply iterator to clone of structure instead. -- (from ARRAYED_LIST) require -- from TRAVERSABLE action_exists: action /= Void do_all_with_index (action: PROCEDURE [PROCEDURE [EVENT_DATA], INTEGER_32]) -- Apply action to every item, from first to last. -- action receives item and its index. -- Semantics not guaranteed if action changes the structure; -- in such a case, apply iterator to clone of structure instead. -- (from ARRAYED_LIST) require -- from ARRAYED_LIST action_not_void: action /= Void do_if (action: PROCEDURE [PROCEDURE [EVENT_DATA]]; test: FUNCTION [PROCEDURE [EVENT_DATA], BOOLEAN]) -- Apply action to every item that satisfies test, from first to last. -- Semantics not guaranteed if action or test changes the structure; -- in such a case, apply iterator to clone of structure instead. -- (from ARRAYED_LIST) require -- from TRAVERSABLE action_exists: action /= Void test_exists: test /= Void do_if_with_index (action: PROCEDURE [PROCEDURE [EVENT_DATA], INTEGER_32]; test: FUNCTION [PROCEDURE [EVENT_DATA], INTEGER_32, BOOLEAN]) -- Apply action to every item that satisfies test, from first to last. -- action and test receive the item and its index. -- Semantics not guaranteed if action or test changes the structure; -- in such a case, apply iterator to clone of structure instead. -- (from ARRAYED_LIST) require -- from ARRAYED_LIST action_not_void: action /= Void test_not_void: test /= Void for_all (test: FUNCTION [PROCEDURE [EVENT_DATA], BOOLEAN]): BOOLEAN -- Is test true for all items? -- (from ARRAYED_LIST) require -- from TRAVERSABLE test_exists: test /= Void ensure then -- from LINEAR empty: is_empty implies Result there_exists (test: FUNCTION [PROCEDURE [EVENT_DATA], BOOLEAN]): BOOLEAN -- Is test true for at least one item? -- (from ARRAYED_LIST) require -- from TRAVERSABLE test_exists: test /= Void feature -- Output Io: STD_FILES -- Handle to standard file setup -- (from ANY) ensure -- from ANY instance_free: class io_not_void: Result /= Void out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) ensure -- from ANY out_not_void: Result /= Void print (o: detachable ANY) -- Write terse external representation of o -- on standard output. -- (from ANY) ensure -- from ANY instance_free: class frozen tagged_out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) ensure -- from ANY tagged_out_not_void: Result /= Void feature -- Platform Operating_environment: OPERATING_ENVIRONMENT -- Objects available from the operating system -- (from ANY) ensure -- from ANY instance_free: class operating_environment_not_void: Result /= Void feature -- Retrieval correct_mismatch -- Attempt to correct object mismatch using Mismatch_information. -- (from ARRAYED_LIST) invariant is_aborted_stack_not_void: is_aborted_stack /= Void call_buffer_not_void: call_buffer /= Void valid_state: state = Normal_state or state = Paused_state or state = Blocked_state call_buffer_consistent: state = Normal_state implies call_buffer.is_empty not_empty_actions_not_void: not_empty_actions /= Void empty_actions_not_void: empty_actions /= Void -- from ARRAYED_LIST prunable: prunable starts_from_one: Lower = 1 -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from RESIZABLE increase_by_at_least_one: Minimal_increase >= 1 -- from BOUNDED valid_count: count <= capacity full_definition: full = (count = capacity) -- from FINITE empty_definition: is_empty = (count = 0) -- from LIST before_definition: before = (index = 0) after_definition: after = (index = count + 1) -- from CHAIN non_negative_index: index >= 0 index_small_enough: index <= count + 1 off_definition: off = ((index = 0) or (index = count + 1)) isfirst_definition: isfirst = ((not is_empty) and (index = 1)) islast_definition: islast = ((not is_empty) and (index = count)) item_corresponds_to_index: (not off) implies (item = i_th (index)) -- from ACTIVE writable_constraint: writable implies readable empty_constraint: is_empty implies (not readable) and (not writable) -- from READABLE_INDEXABLE consistent_boundaries: Lower <= count or else Lower = count + 1 -- from BILINEAR not_both: not (after and before) before_constraint: before implies off -- from LINEAR after_constraint: after implies off -- from TRAVERSABLE empty_constraint: is_empty implies off note library: "EiffelBase: Library of reusable components for Eiffel." copyright: "Copyright (c) 1984-2018, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" source: "[ Eiffel Software 5949 Hollister Ave., 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 ACTION_SEQUENCE
Generated by ISE EiffelStudio