# Extract the content from the given source
	fun extract(source: String): String
	do
		return source.substring(pos_start, pos_end-pos_start+1)
	end