indexing
	description: "[
					Launch processes and redirect output:
					  - Use `spawn' to launch a process asynchronously.
					  		Note: you cannot retrieve the ouput from a
					  		process that was spawned
					  - Use `launch' to launch a process synchronously
					  		and process its output if needed.
	]"
	status: "See notice at end of class"
	date: "$Date$"
	revision: "$Revision$"

class interface
	WEL_PROCESS_LAUNCHER

feature -- Access

	last_launch_successful: BOOLEAN
			-- Was last call to launch successful (i.e. was process started)?

	last_process_result: INTEGER
			-- Last launched process return value
	
feature -- Basic Operations

	launch (a_command_line, a_working_directory: STRING; a_output_handler: ROUTINE [ANY, TUPLE [STRING]])
			-- Launch process described in a_command_line from a_working_directory.
			-- Wait for end of process and send output to a_output_handler if not void.
		require
			non_void_command_line: a_command_line /= void
			valid_command_line: not a_command_line.is_empty
			non_void_working_directory: a_working_directory /= void

	launch_and_refresh (a_command_line, a_working_directory: STRING; a_refresh_handler: ROUTINE [ANY, TUPLE])
			-- Launch process described in a_command_line from a_working_directory.
			-- Calls a_refresh_handler regularly while waiting for end of process.
		require
			non_void_command_line: a_command_line /= void
			valid_command_line: not a_command_line.is_empty
			non_void_working_directory: a_working_directory /= void

	spawn (a_command_line, a_working_directory: STRING)
			-- Spawn asynchronously process described in a_command_line from a_working_directory.
		require
			non_void_command_line: a_command_line /= void
			valid_command_line: not a_command_line.is_empty
			non_void_working_directory: a_working_directory /= void
	
invariant

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

end -- class WEL_PROCESS_LAUNCHER