more robust multithreading;
authorwenzelm
Sat, 05 Nov 2016 20:44:47 +0100
changeset 64466 2bf4fdcebd49
parent 64465 73069f272f42
child 64467 91c98a58985b
more robust multithreading;
src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Nov 05 15:07:11 2016 +0100
+++ b/src/Pure/Admin/build_history.scala	Sat Nov 05 20:44:47 2016 +0100
@@ -11,8 +11,6 @@
 import java.time.format.DateTimeFormatter
 import java.util.Locale
 
-import scala.collection.mutable
-
 
 object Build_History
 {
@@ -420,7 +418,7 @@
 
     /* Admin/build_history */
 
-    val result = new mutable.ListBuffer[(String, Bytes)]
+    var result = Synchronized(List.empty[(String, Bytes)])
 
     def progress_stdout(line: String)
     {
@@ -428,7 +426,7 @@
       val res = (log.base.implode, ssh.read_bytes(log))
       ssh.rm(log)
       progress_result(res._1, res._2)
-      result += res
+      result.change(res :: _)
     }
 
     val process_result =
@@ -439,6 +437,6 @@
         progress_stderr = progress.echo(_),
         strict = false)
 
-    (result.toList, process_result)
+    (result.value.reverse, process_result)
   }
 }