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

kernel.spec.ise

Class KL_DIRECTORY


Direct ancestors

KI_DIRECTORY, KL_SHARED_FILE_SYSTEM, KL_IMPORTED_STRING_ROUTINES, KL_IMPORTED_ANY_ROUTINES, KL_IMPORTED_ARRAY_ROUTINES, DIRECTORY

Creation

Features

Invariants

indexing

description

Filesystem's directories

library

Gobo Eiffel Kernel Library

copyright

Copyright (c) 1999-2001, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/07/13 17:05:05 $

revision

$Revision: 1.29 $

class

KL_DIRECTORY

inherit

KI_DIRECTORY

create

make (a_name: STRING)

-- Create a new directory object.
-- (a_name should follow the pathname convention
-- of the underlying platform. For pathname conversion
-- use KI_FILE_SYSTEM.pathname_from_file_system.)

-- (From KI_FILE_SYSTEM_ENTRY)

require
a_name_not_void: a_name /= Void
ensure
name_set: name = a_name
is_closed: is_closed

feature -- Initialization

reset (a_name: STRING)

-- Reuse current Eiffel object memory to
-- represent a new file system entry.
-- (a_name should follow the pathname convention
-- of the underlying platform. For pathname conversion
-- use KI_FILE_SYSTEM.pathname_from_file_system.)

-- (From KI_FILE_SYSTEM_ENTRY)

require
a_name_not_void: a_name /= Void
is_closed: is_closed
ensure
name_set: name = a_name
is_closed: is_closed

feature -- Access

directory_names: ARRAY [STRING]

-- Names of readable subdirectories in current directory;
-- Void if current directory could not be searched
-- (Do not include parent and current directory names.)

-- (From KI_DIRECTORY)

filenames: ARRAY [STRING]

-- Names of readable files in current directory;
-- Void if current directory could not be searched

-- (From KI_DIRECTORY)

last_entry: STRING

-- Last entry (file or subdirectory name) read
-- (Note: this query returns the new object after
-- each call to read_entry.)

-- (From KI_INPUT_STREAM)

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
name: STRING

-- Directory name;
-- Note: If name is a UC_STRING or descendant, then
-- the bytes of its associated UTF unicode encoding will
-- be used.

-- (From KI_FILE_SYSTEM_ENTRY)

ensure
name_not_void: Result /= Void

feature -- Status report

end_of_input: BOOLEAN

-- Have all entries been read?

-- (From KI_INPUT_STREAM)

require
is_open_read: is_open_read
exists: BOOLEAN

-- Does directory physically exist on disk?
-- (Note that with SmartEiffel this routine
-- actually returns is_readable.)

-- (From KI_FILE_SYSTEM_ENTRY)

is_closable: BOOLEAN

-- Can current file system entry be closed?

-- (From KI_FILE_SYSTEM_ENTRY)

ensure
definition: Result = is_open
is_closed: BOOLEAN

-- Is current directory closed?

-- (From KI_FILE_SYSTEM_ENTRY)

ensure
definition: Result = not is_open
is_open_read: BOOLEAN

-- Has directory been opened in read mode?

-- (From KI_FILE_SYSTEM_ENTRY)

is_readable: BOOLEAN

-- Can directory be opened in read mode?

-- (From KI_FILE_SYSTEM_ENTRY)

ensure
exists: Result implies exists
is_rewindable: BOOLEAN

-- Can current input stream be rewound to return input from
-- the beginning of the stream?

-- (From KI_INPUT_STREAM)

ensure
rewind_implies_open: Result implies is_open_read
valid_unread_entry (an_entry: STRING): BOOLEAN

-- Can an_entry be put back in input stream?

-- (From KI_INPUT_STREAM)

ensure then
an_entry_not_void: Result implies an_entry /= Void
an_entry_not_empty: Result implies an_entry.count > 0

feature -- Basic operations

close

-- Close directory if it is closable,
-- let it open otherwise.

-- (From KI_FILE_SYSTEM_ENTRY)

require
is_closable: is_closable
create_directory

-- Create current directory on disk.
-- Do nothing if the directory could not
-- be created, if it already existed or if
-- name is a nested directory name and
-- the parent directory does not exist.

-- (From KI_DIRECTORY)

require
is_closed: is_closed
delete

-- Delete current directory.
-- Do nothing if the directory could not
-- be deleted, if it did not exist or if
-- it is not empty.

-- (From KI_FILE_SYSTEM_ENTRY)

require
is_closed: is_closed
open_read

-- Try to open directory in read mode. Set is_open_read
-- to true and is ready to read first entry in directory
-- if operation was successful.

-- (From KI_FILE_SYSTEM_ENTRY)

require
is_closed: is_closed
ensure then
not_end_of_input: is_open_read implies not end_of_input
recursive_copy_directory (new_name: STRING)

-- Copy recursively current directory to new_name.
-- Do nothing if the directory could not be copied,
-- if it did not exist, or if new_name already existed.
-- (new_name should follow the pathname convention
-- of the underlying platform. For pathname conversion
-- use KI_FILE_SYSTEM.pathname_from_file_system.)

-- (From KI_DIRECTORY)

require
new_name_not_void: new_name /= Void
is_closed: is_closed
recursive_create_directory

-- Create current directory on disk.
-- Create its parent directories if they do not exist yet.
-- Do nothing if the directory could not be created,
-- if it already existed or name is a nested directory
-- name and its parent directory does not exist and
-- could not be created.

-- (From KI_DIRECTORY)

require
is_closed: is_closed
recursive_delete

-- Delete current directory, its files
-- and its subdirectories recursively.
-- Do nothing if the directory could not
-- be deleted, if it did not exist.

-- (From KI_DIRECTORY)

require
is_closed: is_closed
rewind

-- Move input position to the beginning of stream.

-- (From KI_INPUT_STREAM)

require
can_rewind: is_rewindable

feature -- Input

read_entry

-- Read next entry in directory.
-- Make result available in last_entry.

-- (From KI_INPUT_STREAM)

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
ensure then
last_entry_not_void: not end_of_input implies last_entry /= Void
last_entry_not_empty: not end_of_input implies last_entry.count > 0
read_to_buffer (a_buffer: KI_BUFFER [STRING]pos, nb: INTEGER): INTEGER

-- Fill a_buffer, starting at position pos, with
-- at most nb items read from input stream.
-- Return the number of items actually read.

-- (From KI_INPUT_STREAM)

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
a_buffer_not_void: a_buffer /= Void
pos_large_enough: pos >= 1
nb_large_enough: nb > 0
enough_space: (pos + nb - 1) <= a_buffer.count
ensure
nb_item_read_large_enough: Result >= 0
nb_item_read_small_enough: Result <= nb
not_end_of_input: not end_of_input implies Result > 0
unread_entry (an_entry: STRING)

-- Put an_entry back in input stream.
-- This entry will be read first by the next
-- call to a read routine.

-- (From KI_INPUT_STREAM)

require
is_open_read: is_open_read
an_item_valid: valid_unread_item (an_item)
ensure
not_end_of_input: not end_of_input
last_item_set: last_item = an_item

invariant

string_name_is_string: ANY_.same_types (string_name,
)
no_void_bufferred_entry: entry_buffer /= Void implies entry_buffer.item /= Void

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

end