indexing
	description: "Information about proxies"
	status: "See notice at end of class"
	author: "Patrick Schoenbach"
	date: "$Date$"
	revision: "$Revision$"

class interface
	PROXY_INFORMATION

create 

	make (h: STRING; p: INTEGER)
			-- Create proxy information for host h and port p.
		require
			host_not_empty: h /= void and then not h.is_empty
			host_valid: proxy_host_ok (h)
			port_number_non_negative: p >= 0
		ensure
			host_set: host = h
			port_set: port = p

feature -- Access

	host: STRING
			-- Name or address of proxy host

	port: INTEGER
			-- Port of proxy
	
feature -- Status report

	proxy_host_ok (h: STRING): BOOLEAN
			-- Is h a valid host?
			-- (from HOST_VALIDITY_CHECKER)
	
feature -- Status setting

	set_host (h: STRING)
			-- Set host name to h.
		require
			host_not_empty: h /= void and then not h.is_empty
			host_valid: proxy_host_ok (h)
		ensure
			host_set: host = h

	set_port (p: INTEGER)
			-- Set port to p.
		require
			port_non_negative: p >= 0
		ensure
			port_set: port = p
	
invariant

	host_not_empty: host /= void and then not host.is_empty
	host_valid: proxy_host_ok (host)
	port_non_negative: port >= 0
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)

end -- class PROXY_INFORMATION