more frugal line termination, to cope with huge log files (see also 016cb7d8f297);

--- a/src/Pure/Tools/build.scala	Tue May 14 14:17:56 2013 +0200
+++ b/src/Pure/Tools/build.scala	Tue May 14 15:40:18 2013 +0200
@@ -772,7 +772,7 @@
                 val sources = make_stamp(name)
                 val heap = heap_stamp(job.output_path)
                 File.write_gzip(output_dir + log_gz(name),
-                  sources + "\n" + parent_heap + "\n" + heap + "\n" + res.out)
+                  Library.terminate_lines(sources :: parent_heap :: heap :: res.out_lines))
 
                 heap
               }
@@ -780,7 +780,7 @@
                 (output_dir + Path.basic(name)).file.delete
                 (output_dir + log_gz(name)).file.delete
 
-                File.write(output_dir + log(name), res.out)
+                File.write(output_dir + log(name), Library.terminate_lines(res.out_lines))
                 progress.echo(name + " FAILED")
                 if (res.rc != 130) {
                   progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")

--- a/src/Pure/library.scala	Tue May 14 14:17:56 2013 +0200
+++ b/src/Pure/library.scala	Tue May 14 15:40:18 2013 +0200
@@ -77,6 +77,12 @@
 
   /* lines */
 
+  def terminate_lines(lines: Iterable[CharSequence]): Iterable[CharSequence] =
+    new Iterable[CharSequence] {
+      def iterator: Iterator[CharSequence] =
+        lines.iterator.map(line => new Line_Termination(line))
+    }
+
   def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
@@ -109,7 +115,7 @@
   def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
 
 
-  /* reverse CharSequence */
+  /* CharSequence */
 
   class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
   {
@@ -133,6 +139,16 @@
     }
   }
 
+  class Line_Termination(text: CharSequence) extends CharSequence
+  {
+    def length: Int = text.length + 1
+    def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i)
+    def subSequence(i: Int, j: Int): CharSequence =
+      if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1))
+      else text.subSequence(i, j)
+    override def toString: String = text.toString + "\n"
+  }
+
 
   /* Java futures */