note
	description: "A result for a failed verification."
	date: "$Date$"
	revision: "$Revision$"

class
	E2B_AUTOPROOF_ERROR

inherit

	E2B_VERIFICATION_RESULT
		redefine
			is_equal
		end

	E2B_SHARED_CONTEXT
		redefine
			is_equal
		end

feature -- Access

	type: STRING
			-- Type of error.

	single_line_message (a_formatter: TEXT_FORMATTER)
			-- Single line description of this result.
		do
			a_formatter.add (internal_message)
		end

	context_line_number: INTEGER
			-- Line number of error (if any)

	is_warning: BOOLEAN
			-- Should verification proceed if this error occurs?

feature -- Element change

	set_type (a_string: STRING)
			-- Set `type' to `a_type'.
		do
			type := a_string
		end

	set_message (a_string: READABLE_STRING_32)
			-- Set `single_line_message' to `a_string'.
		do
			internal_message := a_string
		end

	set_line_number (a_value: INTEGER)
			-- Set `context_line_number' to `a_value'.
		do
			context_line_number := a_value
		end

	set_warning (a_flag: BOOLEAN)
			-- Set `is_warning' to `a_flag'
		do
			is_warning := a_flag
		end

feature -- Comparison

	is_equal (a_other: like Current): BOOLEAN
			-- Does `a_other' represent the same error in the same context?
		do
			Result := type ~ a_other.type and
				helper.is_same_class (context_class, a_other.context_class) and
				helper.is_same_feature (context_feature, a_other.context_feature) and
				context_line_number = a_other.context_line_number and
				internal_message ~ a_other.internal_message
		end

feature {E2B_AUTOPROOF_ERROR} -- Implementation

	internal_message: READABLE_STRING_32
			-- Message for this error.

end