class interface F_FILE_SYSTEM

creation
   make
      --  Create object.


feature(s) from F_FILE_SYSTEM
   --  File system

   free_disk_space (drivename: STRING): INTEGER
      --  Return free disk space in KILOBYTES (1024 bytes).

      require
         valid_str: drivename /= Void
      ensure
         done:  --  last_success implies last_size set 

feature(s) from F_FILE_SYSTEM
   --  Directories

   is_directory (pathname: STRING): BOOLEAN
      --  Is pathname a file directory?

      require
         valid_str: pathname /= Void

   create_directory (pathname: STRING)
      --  Create directory pathname.

      require
         valid_str: pathname /= Void;
         not_dir: not is_directory(pathname)
      ensure
         done: last_success implies is_directory(pathname)

   remove_directory (pathname: STRING)
      --  Remove directory pathname.

      require
         valid_str: pathname /= Void;
         not_dir: is_directory(pathname); --  is_empty_directory (pathname)
         empty: 
      ensure
         done: last_success implies not is_directory(pathname)

   directory_content (pattern: STRING)
      --  Get list of files and directories in this directory.
      --  May include * and ? wildcards.

      require
         valid_str: pattern /= Void
      ensure
         done: last_success implies last_content /= Void --  and set.

   current_directory
      --  Get current directory.

      ensure
         done:  --  last_success implies last_directory set

   change_current_directory (newdir: STRING)
      --  Change current directory.


   temporary_directory
      --  Get temporary directory.


feature(s) from F_FILE_SYSTEM
   --  File

   is_file (fname: STRING): BOOLEAN
      --  Does the file fname exists?

      require
         valid_str: fname /= Void

   delete_file (fname: STRING)
      --  Remove file fname.

      require
         valid_str: fname /= Void;
         exists: is_file(fname); --  not is_open (fname)
         not_used: 
      ensure
         done: last_success implies not is_file(fname)

   copy_file (orig_file, dest_file: STRING)
      --  Copy orig_file to dest_file.

      require
         valid_str: orig_file /= Void and dest_file /= Void;
         exists: is_file(orig_file);
         no_existing_dest: not is_file(dest_file)
      ensure
         done: last_success implies is_file(dest_file)

   move_file (orig_file, dest_file: STRING)
      --  Move orig_file to dest_file.

      require
         valid_str: orig_file /= Void and dest_file /= Void;
         exists: is_file(orig_file);
         no_existing_dest: not is_file(dest_file); --  not is_open (orig_name)
         not_used: 
      ensure
         done: last_success implies is_file(dest_file) and not is_file(orig_file)

feature(s) from F_FILE_SYSTEM
   --  Status

   last_success: BOOLEAN
      --  Was the last operation successful?


   last_size: INTEGER
      --  Result of last free_disk_space operation.

      require
         ok: last_success = true
      ensure
         done: Result >= 0

   last_directory: STRING
      --  Result of last system directory request such 
      --  as current_directory.

      require
         ok: last_success = true
      ensure
         done: Result /= Void

   last_content: DS_LIST[STRING]
      --  Result of last of directory_content.

      require
         ok: last_success = true
      ensure
         done: Result /= Void

   last_error: INTEGER
      --  Operating system last error code.

      require
         failed: last_success = false


end of F_FILE_SYSTEM