indexing
	description: "Windows pipe, used in WEL_PROCESS_LAUNCHER"

class interface
	WEL_PIPE

create 

	make
			-- Initialize pipe.

feature -- Status setting

	close
			-- Close pipe.
		require
			output_open: not output_closed
			input_open: not input_closed

	close_input
			-- Close pipe input.
		require
			input_open: not input_closed

	close_output
			-- Close pipe output.
		require
			output_open: not output_closed
	
feature -- Input

	put_string (a_string: STRING)
			-- Write a_string to pipe.
			-- Put number of written bytes in last_written_bytes.
		require
			non_void_string: a_string /= void
			input_open: not input_closed
	
feature -- Output

	read_stream (count: INTEGER)
			-- Read a string of at most count bound characters
			-- or until end of pipe is encountered.
			-- Put number of read bytes in last_read_bytes.
			-- Make result available in last_string.
		require
			valid_count: count > 0
			output_open: not output_closed
	
feature -- Status Report

	exists: BOOLEAN
			-- Does pipe exist?

	input_closed: BOOLEAN
			-- Is pipe input closed?

	input_handle: INTEGER
			-- Pipe output handle

	last_read_bytes: INTEGER
			-- Last amount of bytes read from pipe

	last_read_successful: BOOLEAN
			-- Was last read operation successful?

	last_string: STRING
			-- Last read string

	last_write_successful: BOOLEAN
			-- Was last write operation successful?

	last_written_bytes: INTEGER
			-- Last amount of bytes written to pipe

	output_closed: BOOLEAN
			-- Is pipe output closed?

	output_handle: INTEGER
			-- Pipe input handle
	
invariant

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

end -- class WEL_PIPE