indexing
status: "See notice at end of class"
date: "$Date$"
revision: "$Revision$"
access: execute, immediate, prepare
product: eiffelstore
database: all_bases
class interface
DB_EXEC
create
make
ensure
execution_status: not immediate_execution
feature
immediate_execution: BOOLEAN
is_tracing: BOOLEAN
trace_output: FILE
ensure
destination_file_present: Result = io.error
feature
set_immediate
immediate_executiontrue
ensure
execution_status: immediate_execution
set_trace
ensure
trace_status: is_tracing
unset_immediate
immediate_executionfalse
PREPAREEXECUTE
ensure
execution_status: not immediate_execution
unset_trace
ensure
trace_status: not is_tracing
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- DB_EXEC