# HG changeset patch
# User wenzelm
# Date 1585906184 -7200
# Node ID c87e0d81594d5d9e25eb1b0e1d07219630f6b217
# Parent  12ebd8d0deee550d3ada44e6450738c66e4b75e1
clarified signature;

diff -r 12ebd8d0deee -r c87e0d81594d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Apr 03 11:22:51 2020 +0200
+++ b/src/Pure/Tools/build.scala	Fri Apr 03 11:29:44 2020 +0200
@@ -150,10 +150,11 @@
 
   /* PIDE protocol handler */
 
-  class Handler(progress: Progress, session: Session, session_name: String)
+  private class Protocol_Handler(progress: Progress, session: Session, session_name: String)
     extends Session.Protocol_Handler
   {
-    val build_session_errors: Promise[List[String]] = Future.promise
+    private val build_session_errors: Promise[List[String]] = Future.promise
+    def build_session_join: List[String] = build_session_errors.join
 
     override def exit() { build_session_errors.cancel }
 
@@ -253,7 +254,7 @@
         if (options.bool("pide_build")) {
           val resources = new Resources(sessions_structure, deps(parent))
           val session = new Session(options, resources)
-          val handler = new Handler(progress, session, session_name)
+          val handler = new Protocol_Handler(progress, session, session_name)
           session.init_protocol_handler(handler)
 
           val stdout = new StringBuilder(1000)
@@ -299,7 +300,7 @@
             Exn.capture { process.await_startup } match {
               case Exn.Res(_) =>
                 session.protocol_command("build_session", args_yxml)
-                handler.build_session_errors.join
+                handler.build_session_join
               case Exn.Exn(exn) => List(Exn.message(exn))
             }