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

kernel.io

Class KI_DIRECTORY


Direct ancestors

KI_FILE_SYSTEM_ENTRY, KI_INPUT_STREAM

Known direct descendants

KL_DIRECTORY

Features

Invariants

indexing

description

Interface for directories

library

Gobo Eiffel Kernel Library

copyright

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

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/03/07 04:06:57 $

revision

$Revision: 1.15 $

deferred class

KI_DIRECTORY

inherit

KI_FILE_SYSTEM_ENTRY
KI_INPUT_STREAM

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.)

filenames: ARRAY [STRING]

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

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

-- Name of input stream

-- (From KI_FILE_SYSTEM_ENTRY)

ensure
name_not_void: Result /= Void

feature -- Status report

end_of_input: BOOLEAN

-- Has the end of input stream been reached?

-- (From KI_INPUT_STREAM)

require
is_open_read: is_open_read
exists: BOOLEAN

-- Does file system entry 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 file system entry closed?

-- (From KI_FILE_SYSTEM_ENTRY)

ensure
definition: Result = not is_open
is_open_read: BOOLEAN

-- Can items be read from input stream?

-- (From KI_FILE_SYSTEM_ENTRY)

is_readable: BOOLEAN

-- Can file system entry 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

-- Try to close input stream if it is closable. Set
-- is_open_read to false if operation was successful.

-- (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.

require
is_closed: is_closed
delete

-- Delete current file system entry.
-- Do nothing if the entry could not be deleted
-- (for example if the entry does not exist or
-- if a directory 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.)

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.

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.

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_item: STRING)

-- Put an_item back in input stream.
-- This item 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


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

end