indexing
description: "File name abstraction"
class interface
FILE_NAME
create
make
-- Create path name object.
-- (from PATH_NAME)
make_from_string (p: STRING)
-- Create path name object and initialize it with the
-- path name p
-- (from PATH_NAME)
ensure -- from PATH_NAME
valid_file_name: is_valid
feature -- Initialization
make
-- Create path name object.
-- (from PATH_NAME)
make_from_string (p: STRING)
-- Create path name object and initialize it with the
-- path name p
-- (from PATH_NAME)
ensure -- from PATH_NAME
valid_file_name: is_valid
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is the path name equal to other?
-- (from PATH_NAME)
require -- COMPARABLE
precursor: True
require -- from GENERAL
other_not_void: other /= void
ensure then -- from COMPARABLE
trichotomy: Result = (not (Current < other) and not (other < Current))
ensure -- from GENERAL
symmetric: Result implies other.is_equal (Current);
feature {ANY} -- Status report
empty: BOOLEAN
-- Is structure empty?
-- (from FINITE)
feature {ANY} -- Removal
wipe_out
-- Remove all characters.
-- (from STRING)
require -- from COLLECTION
prunable
ensure -- from COLLECTION
wiped_out: empty
feature {ANY} -- Conversion
frozen to_c: ANY
-- A reference to a C form of current string.
-- Useful only for interfacing with C software.
-- (from STRING)
feature
add_extension (ext: STRING)
-- Append the extension ext to the file name
require
string_exists: ext /= void;
non_empty_extension: not ext.empty;
valid_extension: is_extension_valid (ext)
extend (directory_name: STRING)
-- Append the subdirectory directory_name to the path name.
-- Was declared in PATH_NAME as synonym of extend and set_subdirectory.
-- (from PATH_NAME)
require -- from PATH_NAME
string_exists: directory_name /= void;
valid_directory_name: is_directory_name_valid (directory_name)
ensure -- from PATH_NAME
valid_file_name: is_valid
extend_from_array (directories: ARRAY [STRING])
-- Append the subdirectories from directories to the path name.
-- (from PATH_NAME)
require -- from PATH_NAME
array_exists: directories /= void and then not (directories.empty)
ensure -- from PATH_NAME
valid_file_name: is_valid
is_directory_name_valid (dir_name: STRING): BOOLEAN
-- Is dir_name a valid subdirectory part for the operating system?
-- (from PATH_NAME)
require -- from PATH_NAME
exists: dir_name /= void
is_extension_valid (ext: STRING): BOOLEAN
-- Is ext a valid extension for the operating system?
is_file_name_valid (f_name: STRING): BOOLEAN
-- Is f_name a valid file name part for the operating system?
is_valid: BOOLEAN
-- Is the file name valid for the operating system?
is_volume_name_valid (vol_name: STRING): BOOLEAN
-- Is vol_name a valid volume name for the operating system?
-- (from PATH_NAME)
require -- from PATH_NAME
exists: vol_name /= void
set_directory (directory_name: STRING)
-- Set the absolute directory part of the path name to directory_name.
-- (from PATH_NAME)
require -- from PATH_NAME
string_exists: directory_name /= void;
valid_directory_name: is_directory_name_valid (directory_name)
ensure -- from PATH_NAME
valid_file_name: is_valid
set_file_name (file_name: STRING)
-- Set the value of the file name part.
require
string_exists: file_name /= void;
valid_file_name: is_file_name_valid (file_name)
ensure
valid_file_name: is_valid
set_subdirectory (directory_name: STRING)
-- Append the subdirectory directory_name to the path name.
-- Was declared in PATH_NAME as synonym of extend and set_subdirectory.
-- (from PATH_NAME)
require -- from PATH_NAME
string_exists: directory_name /= void;
valid_directory_name: is_directory_name_valid (directory_name)
ensure -- from PATH_NAME
valid_file_name: is_valid
set_volume (volume_name: STRING)
-- Set the volume part of the path name to volume_name.
-- (from PATH_NAME)
require -- from PATH_NAME
string_exists: volume_name /= void;
valid_volume_name: is_volume_name_valid (volume_name);
empty_path_name: empty
ensure -- from PATH_NAME
valid_file_name: is_valid
invariant
-- from COMPARABLE
irreflexive_comparison: not (Current < Current);
end -- class FILE_NAME