# HG changeset patch
# User wenzelm
# Date 1456355928 -3600
# Node ID 13a0f537e232884a2346d5eed8ba683a304b7949
# Parent  1d7aba20a332345156a951f7d91f1c7681308ee3
retain tail out_lines as printed, but not the whole log content;

diff -r 1d7aba20a332 -r 13a0f537e232 src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Thu Feb 25 00:06:37 2016 +0100
+++ b/src/Pure/System/process_result.scala	Thu Feb 25 00:18:48 2016 +0100
@@ -28,12 +28,10 @@
     else if (interrupted) throw Exn.Interrupt()
     else Library.error(err)
 
-  def clear: Process_Result = copy(out_lines = Nil, err_lines = Nil)
-
   def print: Process_Result =
   {
     Output.warning(Library.trim_line(err))
     Output.writeln(Library.trim_line(out))
-    clear
+    copy(out_lines = Nil, err_lines = Nil)
   }
 }
diff -r 1d7aba20a332 -r 13a0f537e232 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Feb 25 00:06:37 2016 +0100
+++ b/src/Pure/Tools/build.scala	Thu Feb 25 00:18:48 2016 +0100
@@ -875,6 +875,14 @@
             val process_result = job.join
             progress.echo(process_result.err)
 
+            val process_result_tail =
+            {
+              val lines = process_result.out_lines.filterNot(_.startsWith("\f"))
+              val tail = lines.drop(lines.length - 20 max 0)
+              process_result.copy(out_lines =
+                "(see also " + (output_dir + log(name)).file.toString + ")" :: tail)
+            }
+
             val heap =
               if (process_result.ok) {
                 (output_dir + log(name)).file.delete
@@ -892,17 +900,12 @@
 
                 File.write(output_dir + log(name), Library.terminate_lines(process_result.out_lines))
                 progress.echo(name + " FAILED")
-                if (!process_result.interrupted) {
-                  progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
-                  val lines = process_result.out_lines.filterNot(_.startsWith("\f"))
-                  val tail = lines.drop(lines.length - 20 max 0)
-                  progress.echo("\n" + cat_lines(tail))
-                }
+                if (!process_result.interrupted) progress.echo(process_result_tail.out)
 
                 no_heap
               }
             loop(pending - name, running - name,
-              results + (name -> Result(false, heap, Some(process_result.clear))))
+              results + (name -> Result(false, heap, Some(process_result_tail))))
             //}}}
           case None if running.size < (max_jobs max 1) =>
             //{{{ check/start next job