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