Match case insensitively for headers.

Try to recv() Content-Length bytes when specified, and 1024 bytes at a
time when not.
Call js.gc() after each recv().

The gc() call fixes the "out of memory" error which occured on HTTP pages
over about 128KiB and makes reading web pages considerably faster.

exec/load/http.js

@@ -112,18 +112,26 @@ function HTTPRequest(username,password)
 			if(header=='')
 				return;
 			this.response_headers.push(header);
-			m=header.match(/^Content-length:\s+([0-9]+)$/);
+			m=header.match(/^Content-length:\s+([0-9]+)$/i);
 			if(m!=null)
-				this.contentlength=parseInt(m[0]);
+				this.contentlength=parseInt(m[1]);
 		}
 	};
 
 	this.ReadBody=function() {
 		var ch;
+		var lastlen=0;
+		var len=this.contentlength;
+		if(len==undefined)
+			len=1024;
 
 		this.body='';
-		while((ch=this.sock.recv(1))!=null && ch != '') {
-			this.body += ch;
+		while((ch=this.sock.recv(len))!=null && ch != '') {
+			this.body += ch.toString();
+			len -= ch.length;
+			if(len < 1)
+				len=1024;
+			js.gc();
 		}
 	};