src/Pure/Tools/build.scala
changeset 65317 b9f5cd845616
parent 65315 c7097ccbffb7
child 65318 342efc382558
     1.1 --- a/src/Pure/Tools/build.scala	Sat Mar 18 21:40:47 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Sat Mar 18 22:11:05 2017 +0100
     1.3 @@ -225,22 +225,24 @@
     1.4            val handler = new Handler(progress, session, name)
     1.5            session.init_protocol_handler(handler)
     1.6  
     1.7 -          val session_result = Future.promise[Int]
     1.8 +          val session_result = Future.promise[Process_Result]
     1.9  
    1.10            Isabelle_Process.start(session, options, logic = parent,
    1.11              cwd = info.dir.file, env = env, tree = Some(tree), store = store,
    1.12              phase_changed =
    1.13              {
    1.14                case Session.Ready => session.protocol_command("build_session", args_yxml)
    1.15 -              case Session.Terminated(rc) => session_result.fulfill(rc)
    1.16 +              case Session.Terminated(result) => session_result.fulfill(result)
    1.17                case _ =>
    1.18              })
    1.19  
    1.20 -          val rc = session_result.join
    1.21 -
    1.22 +          val result = session_result.join
    1.23            handler.result_error.join match {
    1.24 -            case "" => Process_Result(rc)
    1.25 -            case msg => Process_Result(rc max 1, out_lines = split_lines(Output.error_text(msg)))
    1.26 +            case "" => result
    1.27 +            case msg =>
    1.28 +              result.copy(
    1.29 +                rc = result.rc max 1,
    1.30 +                out_lines = result.out_lines ::: split_lines(Output.error_text(msg)))
    1.31            }
    1.32          }
    1.33          else {