Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

em.goof.loader

Class EM_GOOF_LOADER_LEVEL_FILE


Direct ancestors

KL_SHARED_FILE_SYSTEM, EXCEPTIONS

Creation

Features

Invariants

indexing

description

A EM_GOOF_LOADER level xml file, to read a EM_GOOF_LOADER level from.

date

$Date: 2005/10/23 15:36:59 $

revision

$Revision: 1.4 $

class

EM_GOOF_LOADER_LEVEL_FILE

create

make_from_file (a_filename: STRING)

-- Initialize with level loaded from file with a_filename.
-- (either a_filename is an absolute path
-- or relative to current working directory)

require
a_filename_not_empty: a_filename /= Void and then not a_filename.is_empty
file_with_a_filename_exists: File_system.file_exists (a_filename)
ensure
goof_level_loaded: goof_level /= Void

feature -- Access

filename: STRING

-- Filename

goof_level: EM_GOOF_PHYSICS

-- Map in Current.

invariant

filename_not_empty: filename /= Void and then not filename.is_empty
goof_level_not_void: goof_level /= Void

-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

end