note
	description: "Eiffel class instanciated and used from the Eiffel runtime."
	status: "See notice at end of class."
	legal: "See notice at end of class."
	date: "$Date: 2019-03-20 17:08:56 +0000 (Wed, 20 Mar 2019) $"
	revision: "$Revision: 102984 $"

class interface
	RT_EXTENSION

create 
	default_create

feature -- Notification

	notify (a_id: INTEGER_32; a_data: TUPLE)
			-- Notify operation a_id with data a_data
		require
			a_data_attached: a_data /= Void

	notify_argument (a_id: INTEGER_32): detachable TUPLE
			-- Empty argument container for operation a_id.

	Cached_arguments: ARRAY [detachable TUPLE]
			-- Cached argument to use less temporary objects
		ensure
			result_attached: Result /= Void
	
feature -- Execution replay		

	activate_execution_replay_recording (b: BOOLEAN; ref: ANY; cid: INTEGER_32; fid: INTEGER_32; dep: INTEGER_32; break_index: INTEGER_32)
			-- Start or Stop execution replay recording
		require
			ref_attached: ref /= Void
		ensure
			recorder_if_on: b implies execution_recorder /= Void
			no_recorder_if_off: not b implies execution_recorder = Void
	
feature -- debug purpose: to remove

	test_activate_recording (ref: ANY; fid: INTEGER_32; dep: INTEGER_32; bpline: INTEGER_32)
		require
			ref_attached: ref /= Void

	frozen c_activate_recording

	frozen c_is_inside_rt_eiffel_code: INTEGER_32
	
feature -- SCOOP Access	

	scoop_processor_id_from_object (a_object: ANY): INTEGER_32
			-- SCOOP Processor id for object a_object.
	
invariant
	no_attribute: (create {REFLECTED_REFERENCE_OBJECT}.make (Current)).field_count = 0

note
	library: "EiffelBase: Library of reusable components for Eiffel."
	copyright: "Copyright (c) 1984-2019, 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 RT_EXTENSION

Generated by ISE EiffelStudio