class interface UT_FILENAME_HANDLER creation make -- Create a new filename handler. ensure directory_separators_set: equal(directory_separators,"/\") feature(s) from KL_IMPORTED_STRING_ROUTINES -- Access STRING_: KL_STRING_ROUTINES -- Routines that ought to be in class STRING ensure string_routines_not_void: Result /= Void feature(s) from UT_FILENAME_HANDLER -- Access pathname (a_dirname, a_filename: STRING): STRING -- Pathname made up of a_dirname and a_filename -- and separated by the first directory separator require a_dirname_not_void: a_dirname /= Void; a_filename_not_void: a_filename /= Void ensure pathname_not_void: Result /= Void directory_separators: STRING -- Directory separators feature(s) from UT_FILENAME_HANDLER -- Setting set_directory_separators (separators: STRING) -- Set directory_separators to separators. require separators_not_void: separators /= Void; separators_not_empty: not separators.empty ensure directory_separators_set: directory_separators = separators invariant directory_separators_not_void: directory_separators /= Void; directory_separators_not_empty: not directory_separators.empty; end of UT_FILENAME_HANDLER