indexing
description: "Directories, in the Unix sense, with creation and exploration features"
library: "Free implementation of ELKS library"
copyright: "Copyright (c) 1986-2008, Eiffel Software and others"
license: "Eiffel Forum License v2 (see forum.txt)"
date: "$Date: 2008-05-23 17:24:07 -0700 (Fri, 23 May 2008) $"
revision: "$Revision: 170 $"
class interface
DIRECTORY
create
make (dn: STRING_8)
`dn'
require
string_exists: dn /= Void
make_open_read (dn: STRING_8)
`dn'
require
string_exists: dn /= Void
feature
create_dir
require
physical_not_exists: not exists
make (dn: STRING_8)
`dn'
require
string_exists: dn /= Void
make_open_read (dn: STRING_8)
`dn'
require
string_exists: dn /= Void
feature
change_name (new_name: STRING_8)
name`new_name'
require
new_name_not_void: new_name /= Void
directory_exists: exists
ensure
name_changed: name.is_equal (new_name)
close
require
is_open: not is_closed
generating_type: STRING_8
ANY
ensure ANY
generating_type_not_void: Result /= Void
generating_type_not_empty: not Result.is_empty
generator: STRING_8
ANY
ensure ANY
generator_not_void: Result /= Void
generator_not_empty: not Result.is_empty
has_entry (entry_name: STRING_8): BOOLEAN
`entry_name'
`dir_temp'
require
string_exists: entry_name /= Void
name: STRING_8
open_read
readentry
lastentry
require
is_opened: not is_closed
start
require
is_opened: not is_closed
feature
count: INTEGER_32
require
directory_exists: exists
feature
frozen deep_equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
shallow_implies_deep: standard_equal (some, other) implies Result
both_or_none_void: (some = Void) implies (Result = (other = Void))
same_type: (Result and (some /= Void)) implies (other /= Void and then some.same_type (other))
symmetric: Result implies deep_equal (other, some)
frozen equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))
frozen is_deep_equal (other: DIRECTORY): BOOLEAN
`Current'`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
shallow_implies_deep: standard_is_equal (other) implies Result
same_type: Result implies same_type (other)
symmetric: Result implies other.is_deep_equal (Current)
is_equal (other: DIRECTORY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
frozen standard_equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))
frozen standard_is_equal (other: DIRECTORY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
same_type: Result implies same_type (other)
symmetric: Result implies other.standard_is_equal (Current)
feature
conforms_to (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
exists: BOOLEAN
is_closed: BOOLEAN
is_empty: BOOLEAN
require
directory_exists: exists
is_executable: BOOLEAN
require
directory_exists: exists
is_readable: BOOLEAN
require
directory_exists: exists
is_writable: BOOLEAN
require
directory_exists: exists
lastentry: ?STRING_8
readentry
same_type (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
definition: Result = (conforms_to (other) and other.conforms_to (Current))
feature
delete
require
directory_exists: exists
empty_directory: is_empty
delete_content
require
directory_exists: exists
delete_content_with_action (action: PROCEDURE [ANY, TUPLE]; is_cancel_requested: FUNCTION [ANY, TUPLE, BOOLEAN]; file_number: INTEGER_32)
`action'`file_number'
`action'
`is_cancel_requested'
`True'
`is_cancel_requested'
require
directory_exists: exists
valid_file_number: file_number > 0
dispose
recursive_delete
require
directory_exists: exists
recursive_delete_with_action (action: PROCEDURE [ANY, TUPLE]; is_cancel_requested: FUNCTION [ANY, TUPLE, BOOLEAN]; file_number: INTEGER_32)
`action'`file_number'
require
directory_exists: exists
feature
linear_representation: ARRAYED_LIST [STRING_8]
feature
copy (other: DIRECTORY)
`other'
ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
frozen deep_copy (other: DIRECTORY)
copy`other'deep_twin
ANY
require ANY
other_not_void: other /= Void
ensure ANY
deep_equal: deep_equal (Current, other)
frozen deep_twin: DIRECTORY
ANY
ensure ANY
deep_twin_not_void: Result /= Void
deep_equal: deep_equal (Current, Result)
frozen standard_copy (other: DIRECTORY)
`other'
ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_standard_equal: standard_is_equal (other)
frozen standard_twin: DIRECTORY
`other'
ANY
ensure ANY
standard_twin_not_void: Result /= Void
equal: standard_equal (Result, Current)
frozen twin: DIRECTORY
`Current'
twincopycopy
ANY
ensure ANY
twin_not_void: Result /= Void
is_equal: Result.is_equal (Current)
feature
frozen default: ?DIRECTORY
ANY
frozen default_pointer: POINTER
`POINTER'
`p'default
`p'`POINTER'
ANY
default_rescue
ANY
frozen do_nothing
ANY
feature
io: STD_FILES
ANY
ensure ANY
io_not_void: Result /= Void
out: STRING_8
ANY
ensure ANY
out_not_void: Result /= Void
print (some: ?ANY)
`some'
ANY
frozen tagged_out: STRING_8
ANY
ensure ANY
tagged_out_not_void: Result /= Void
feature
operating_environment: OPERATING_ENVIRONMENT
ANY
ensure ANY
operating_environment_not_void: Result /= Void
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end DIRECTORY