expanded class interface FILE_TOOLS
   -- This expanded class gather tools relatives to files such as 
   -- file comparison, file renaming, file deletion, file size, file 
   -- permissions...
   --
   -- Note this is a facilities class. Files are referenced with 
   -- their names (as STRINGs). Consider using functions available in
   -- TEXT_FILE_READ if you are already connected to the file.

feature(s) from FILE_TOOLS
   same_files (path1, path2: STRING): BOOLEAN
      -- True if the path1 file exists and has the very same content
      -- as file path2.
      require
         path1 /= Void;
         path2 /= Void

   is_readable (path: STRING): BOOLEAN
      -- True if path file exists and is a readable file.
      require
         path /= Void

   is_empty (path: STRING): BOOLEAN
      -- True if path file exists, is readable and is an empty file.

   rename_to (old_path, new_path: STRING)
      -- Try to change the name or the location of a file.
      require
         old_path /= Void;
         new_path /= Void

   delete (path: STRING)
      -- Try to delete the given path file.
      require
         path /= Void

   size_of (path: STRING): INTEGER
      -- Total size of file path in number of bytes.
      require
         file_exists(path)

   last_change_of (path: STRING): TIME
      -- Of the last modification of path.
      require
         file_exists(path)



end of expanded FILE_TOOLS