class WINDOWS_DIRECTORY_NOTATION
Summary
The Windows like file path notation looks like:
  C:\LibertyEiffel\sys\system.se
Direct parents
Inherit list: PATH_NAME_NOTATION
Overview
Features
{ANY}
{ANY}
{}
DIRECTORY_NOTATION interface
{ANY}
{DIRECTORY_NOTATION}
{PATH_JOINER}
  • start_join (drive: STRING, absoluteness: INTEGER_32)
    Start joining an absolute path to Current
    drive is optional absoluteness is, e.g., the number of leading slashes:
      0 for relative paths
      1 for absolute paths
      more for super-absolute paths (for instance, network-wide)
    
  • join_directory (element: STRING)
    Add a directory to the end of the path
  • join_up
    Go up one directory
  • join_file (element: STRING)
    Add a file to the end of the path
  • join_element (element: STRING)
    Add an unspecified element (directory or file) to the end of the path
  • join_extension (an_extension: STRING)
    Add an extension to the last element of the path
  • end_join
    Finish joining the path
  • join_error: BOOLEAN
    Did an error occur during joining
{PATH_NAME_NOTATION}
{}
{ANY}
{ANY}
is_current_directory (path: STRING): BOOLEAN
effective function
{ANY}
is_parent_directory (path: STRING): BOOLEAN
effective function
{ANY}
to_directory_path (path: STRING)
effective procedure
{ANY}
Make sure that the given path is a canonical directory path as would be returned by to_subdirectory_with
require
  • path /= Void
  • is_valid_path(path)
ensure
  • is_valid_directory_path(path)
is_case_sensitive: BOOLEAN
is False
constant attribute
{ANY}
once function
{}
ensure
  • tmp1 /= tmp2
once function
{}
ensure
  • tmp1 /= tmp2
to_parent_directory (some_path: STRING)
effective procedure
{ANY}
Tries to compute in some_path (which may be either a file path or a directory path) the parent directory of some_path.
When some_path is a path with no parent directory, some_path is_empty after this call. This operation does not perform any disk access.
require
  • is_valid_path(some_path)
to_subdirectory_with (parent_path: STRING, entry_name: STRING)
effective procedure
{ANY}
Try to compute in parent_path the new subdirectory path obtained when trying to concatenate smartly parent_path with some entry_name.
When this fails, parent_path is_empty after this call. This operation does not perform any disk access.
require
  • is_valid_path(parent_path)
  • is_valid_path(entry_name)
ensure
  • entry_name.is_equal(old entry_name.twin)
to_file_path_with (parent_path: STRING, file_name: STRING)
effective procedure
{ANY}
Try to compute in parent_path the new file path obtained when trying to concatenate smartly parent_path with some file_name.
When this fails, parent_path is_empty after this call. This operation does not perform any disk access.
require
  • is_valid_path(parent_path)
  • is_valid_file_name(file_name)
ensure
  • file_name.is_equal(old file_name.twin)
to_subpath_with (parent_path: STRING, subpath: STRING)
effective procedure
{ANY}
Try to compute in parent_path the new file path obtained when trying to concatenate smartly parent_path with some subpath.
When this fails, parent_path is_empty after this call. This operation does not perform any disk access.
require
  • is_valid_directory_path(parent_path)
  • is_valid_path(subpath)
  • not is_absolute_path(subpath)
ensure
  • parent_path.is_empty or else is_valid_path(parent_path)
  • parent_path.is_empty or else is_valid_directory_path(parent_path) = old is_valid_directory_path(subpath)
  • parent_path.is_empty or else is_absolute_path(parent_path) = old is_absolute_path(parent_path)
can_map_drive (source_notation: DIRECTORY_NOTATION, drive: STRING): BOOLEAN
effective function
{ANY}
to_root (source_notation: DIRECTORY_NOTATION, drive: STRING)
effective procedure
{ANY}
Convert drive from a drive letter/device name in source_notation to an absolute path in Current notation.
require
  • can_map_drive(source_notation, drive)
ensure
  • is_valid_path(drive)
  • is_absolute_path(drive)
to_default_root (directory: STRING)
effective procedure
{ANY}
ensure
  • is_valid_path(directory)
  • is_absolute_path(directory)
to_current_directory (directory: STRING)
effective procedure
{ANY}
Put the relative directory representing the current working directory into directory.
Not to be confused with the absolute path of the current working directory at a given time. This operation does not perform any disk access.
require
  • directory /= Void
ensure
  • is_valid_path(directory)
  • not is_absolute_path(directory)
is_absolute_path (path: STRING): BOOLEAN
effective function
{ANY}
Is path absolute, i.e.
is its meaning independent of current drive and working directory ? This operation does not perform any disk access.
require
  • is_valid_path(path)
ensure
  • path.is_equal(old path.twin)
is_valid_path (a_path: STRING): BOOLEAN
effective function
{ANY}
Does path represent a syntactically valid file or directory path?
The result does not imply that there actually a file or directory with that name. This operation does not perform any disk access.
ensure
  • a_path.is_equal(old a_path.twin)
  • Result implies not a_path.is_empty
is_valid_directory_path (a_path: STRING): BOOLEAN
effective function
{ANY}
Does path represent a syntactically valid directory path?
For many Systems, there may be no syntactical difference between file paths and directory paths, in that case there is no difference between is_valid_directory_path and is_valid_path.
ensure
  • a_path.is_equal(old a_path.twin)
  • Result implies is_valid_path(a_path)
is_valid_file_name (name: STRING): BOOLEAN
effective function
{ANY}
Does path only contain valid characters for a file?
The result does not imply that there is actually a file or directory with that name. Not the same as is_valid_path: path separators (/ for unix, \ for windows, ...) are allowed in paths, but not in file names. This operation does not perform any disk access.
ensure
  • name.is_equal(old name.twin)
  • Result implies not name.is_empty
to_short_name_in (buffer: STRING, path: STRING)
effective procedure
{ANY}
require
  • is_valid_path(path)
  • buffer /= Void
to_notation (path: STRING, destination: DIRECTORY_NOTATION): STRING
effective function
require
  • is_valid_path(path)
  • destination /= Void
ensure
  • path.is_equal(old path.twin)
  • Result.is_empty or else destination.is_valid_path(Result)
start_join (drive: STRING, absoluteness: INTEGER_32)
effective procedure
Start joining an absolute path to Current
drive is optional absoluteness is, e.g., the number of leading slashes:
  0 for relative paths
  1 for absolute paths
  more for super-absolute paths (for instance, network-wide)
require
  • absoluteness >= 0
join_directory (element: STRING)
effective procedure
Add a directory to the end of the path
require
  • element /= Void
ensure
  • old join_error implies join_error
join_up
effective procedure
Go up one directory
ensure
  • old join_error implies join_error
join_file (element: STRING)
effective procedure
Add a file to the end of the path
require
  • element /= Void
ensure
  • old join_error implies join_error
join_element (element: STRING)
effective procedure
Add an unspecified element (directory or file) to the end of the path
require
  • element /= Void
ensure
  • old join_error implies join_error
join_extension (an_extension: STRING)
effective procedure
Add an extension to the last element of the path
require
  • an_extension /= Void
ensure
  • old join_error implies join_error
end_join
effective procedure
Finish joining the path
ensure
  • old join_error implies join_error
join_error: BOOLEAN
is False
constant attribute
Did an error occur during joining
from_path_name (other: PATH_NAME): STRING
effective function
require
current_path: STRING
writable attribute
{}
destination_notation: DIRECTORY_NOTATION
writable attribute
{}
to_absolute_path_in (possible_parent: STRING, path: STRING)
frozen
effective procedure
{ANY}
If path is not absolute, make it so by appending it to possible_parent.
Else, overwrite possible_parent with path.
require ensure
from_notation (source_notation: DIRECTORY_NOTATION, path: STRING)
frozen
effective procedure
{ANY}
Convert path from source_notation to Current notation.
If this fails, then path is_empty after this call.
require ensure
can_sanitize (name: STRING): BOOLEAN
effective function
{ANY}
to_valid_file_name (name: STRING)
effective procedure
{ANY}
Sanitize name (by removing forbidden characters or encoding them)
require ensure