indexing
	description: "Object used to retrieve total and free disk space on anylocal hard drive. Remote drive are not yet supported"
	status: "See notice at end of class."
	date: "$Date$"
	revision: "$Revision$"

class interface
	WEL_DISK_SPACE

create 

feature -- Access

	last_free_space: INTEGER
			-- Free space available on the last requested drive via the
			-- query query_disk_space. This value is updated by
			-- the feature query_disk_space.
			--
			-- THIS FEATURE RETURNS THE RESULT IN MEGABYTES
			-- Use last_free_space_in_bytes to get an accurate result
			-- in bytes.
		require
			last_query_successful: last_query_success = True

	last_free_space_in_bytes: INTEGER
			-- Free space available on the last requested drive via the
			-- query query_disk_space. This value is updated by
			-- the feature query_disk_space.
			--
			-- This value is only valid if the free disk space
			-- is less than 2 Gb. Otherwise, it cannot be represented
			-- by an INTEGER which is a signed 32 bits value.
		require
			result_meaningfull: last_free_space < 2047
			last_query_successful: last_query_success = True

	last_free_space_in_string: STRING
			-- Compute the string representing the value of the free space
			-- as computed on the last call to query_disk_space.
			-- Example of possible returned strings: "600 Mb", "30.1 Mb", "1.33 Mb",
			-- "320 Kb", "52.7 Kb", "75 bytes", "30 Tb", ...
		require
			last_query_successful: last_query_success = True

	last_query_success: BOOLEAN
			-- Was the last call to query_disk_space successful?

	last_total_space: INTEGER
			-- Total space available on the last requested drive via the
			-- query query_disk_space. This value is updated by
			-- the feature query_disk_space.
			--
			-- THIS FEATURE RETURNS THE RESULT IN MEGABYTES
			-- Use last_total_space_in_bytes to get an accurate result
			-- in bytes.
		require
			last_query_successful: last_query_success = True

	last_total_space_in_bytes: INTEGER
			-- Total space available on the last requested drive via the
			-- query query_disk_space. This value is updated by
			-- the feature query_disk_space.
			--
			-- This value is only valid if the free disk space
			-- is less than 2 Gb. Otherwise, it cannot be represented
			-- by an INTEGER which is a signed 32 bits value.
		require
			result_meaningfull: last_total_space < 2047
			last_query_successful: last_query_success = True

	last_total_space_in_string: STRING
			-- Compute the string representing the value of the total space
			-- as computed on the last call to query_disk_space.
			-- Example of possible returned strings: "600 Mb", "30.1 Mb", "1.33 Mb",
			-- "320 Kb", "52.7 Kb", "75 bytes", "30 Tb", ...
		require
			last_query_successful: last_query_success = True
	
feature -- Status report

	query_local_drive (drive_letter: CHARACTER)
			-- Query the disk space available on the local drice
			-- designated by the letter drive_letter.
	
invariant

		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)

end -- class WEL_DISK_SPACE