indexing
description: "Path name abstraction"
deferred class interface
PATH_NAME
feature -- Initialization
make
-- Create path name object.
make_from_string (p: STRING)
-- Create path name object and initialize it with the
-- path name p
ensure
valid_file_name: is_valid
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is the path name equal to other?
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
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.
require
string_exists: directory_name /= void;
valid_directory_name: is_directory_name_valid (directory_name)
ensure
valid_file_name: is_valid
extend_from_array (directories: ARRAY [STRING])
-- Append the subdirectories from directories to the path name.
require
array_exists: directories /= void and then not (directories.empty)
ensure
valid_file_name: is_valid
is_directory_name_valid (dir_name: STRING): BOOLEAN
-- Is dir_name a valid subdirectory part for the operating system?
require
exists: dir_name /= void
is_valid: BOOLEAN
-- Is the path 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?
require
exists: vol_name /= void
set_directory (directory_name: STRING)
-- Set the absolute directory part of the path name to directory_name.
require
string_exists: directory_name /= void;
valid_directory_name: is_directory_name_valid (directory_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.
require
string_exists: directory_name /= void;
valid_directory_name: is_directory_name_valid (directory_name)
ensure
valid_file_name: is_valid
set_volume (volume_name: STRING)
-- Set the volume part of the path name to volume_name.
require
string_exists: volume_name /= void;
valid_volume_name: is_volume_name_valid (volume_name);
empty_path_name: empty
ensure
valid_file_name: is_valid
invariant
-- from COMPARABLE
irreflexive_comparison: not (Current < Current);
end -- class PATH_NAME