Provide a way to log into a file, rather than just console output

Minor optimization for WSF_LOGGING_FILTER

library/server/wsf/router/filter/wsf_logging_filter.e

@@ -9,31 +9,77 @@ class
 
 inherit
 	WSF_FILTER
+		redefine
+			default_create
+		end
+
+create
+	default_create,
+	make_with_output
+
+feature {NONE} -- Initialization
+
+	default_create
+		do
+			Precursor
+			output := io.output
+		end
+
+	make_with_output (a_output: like output)
+			-- Create Current with `a_output' as `output'
+		require
+			a_output_opened: a_output.is_open_read
+		do
+			default_create
+			output := a_output
+		end
+
+	output: FILE
+			-- Output file
+			--| Could be stdout, or a file...
 
 feature -- Basic operations
 
 	execute (req: WSF_REQUEST; res: WSF_RESPONSE)
 			-- Execute the filter
 		local
-			l_user_agent, l_referer: STRING
 			l_date: DATE_TIME
+			s: STRING
 		do
-			if attached req.http_user_agent as ua then
+			create s.make (64)
-				l_user_agent := "%"" + ua.as_string_8 + "%""
+			s.append (req.remote_addr)
-			else
+			s.append (" - - [")
-				l_user_agent := "-"
-			end
-			if attached req.http_referer as r then
-				l_referer := "%"" + r + "%" "
-			else
-				l_referer := ""
-			end
 			create l_date.make_now_utc
-			io.put_string (req.remote_addr + " - - [" + l_date.formatted_out (Date_time_format) + " GMT] %""
+			s.append (l_date.formatted_out (Date_time_format))
-				+ req.request_method + " " + req.request_uri
+			s.append (" GMT] %"")
-				+ " " + {HTTP_CONSTANTS}.http_version_1_1 + "%" " + res.status_code.out + " "
+			s.append (req.request_method)
-				+ res.transfered_content_length.out + " " + l_referer + l_user_agent)
+			s.append_character (' ')
-			io.put_new_line
+			s.append (req.request_uri)
+			s.append_character (' ')
+			s.append ({HTTP_CONSTANTS}.http_version_1_1)
+			s.append_character ('%"')
+			s.append_character (' ')
+			s.append_integer (res.status_code)
+			s.append_character (' ')
+			s.append_natural_64 (res.transfered_content_length)
+			s.append_character (' ')
+			if attached req.http_referer as r then
+				s.append_character ('%"')
+				s.append_character ('%"')
+				s.append (r)
+				s.append_character (' ')
+			end
+
+			if attached req.http_user_agent as ua then
+				s.append_character ('%"')
+				s.append (ua)
+				s.append_character ('%"')
+			else
+				s.append_character ('-')
+			end
+
+			output.put_string (s)
+			output.put_new_line
 			execute_next (req, res)
 		end