Re: [gobo-eiffel-develop] [Colin Paul Adams] Re: Bug in {RX_REGULAR_EXPRESSION}.replace_all

[Colin P. A. <co...@co...>]

>>>>> "Colin" == Colin Paul Adams <co...@co...> writes:

    Colin> I don't know if that is the correct result to return, but I
    Colin> can't think of any other at the moment.

    Colin> That wasn't sufficient, as the postcondition all_matched
    Colin> doesn't hold. I will have to dig deeper.

This might be better - at least the contract holds:

	replace_all (a_replacement: STRING): STRING is
			-- Substring of `subject' between `subject_start' and `subject_end'
			-- where the whole matched string has been repeatedly replaced by
			-- `a_replacement'; All occurrences of \n\ in `a_replacement' will
			-- have been replaced by the corresponding n-th captured substrings
			-- if any
		require
			is_matching: is_matching
			a_replacement_not_void: a_replacement /= Void
			same_type: ANY_.same_types (a_replacement, subject)
		do
			if subject_end = subject_start then
				Result := STRING_.new_empty_string (subject, subject_end - subject_start)
				append_replace_all_to_string (Result, a_replacement)
			else
				Result := subject
				append_replace_all_to_string (Result, a_replacement)
			end
		ensure
			all_matched: not has_matched
			replace_not_void: Result /= Void
			same_type: ANY_.same_types (Result, subject)
		end
-- 
Colin Adams
Preston Lancashire