# HG changeset patch
# User wenzelm
# Date 1489842758 -3600
# Node ID fd6415b8c0a917e9e549c02973f95632d3367344
# Parent  f2e80ff36b7e7e8956c8b7f95c975c271f5b1a87
clarified result;

diff -r f2e80ff36b7e -r fd6415b8c0a9 src/Pure/PIDE/batch_session.scala
--- a/src/Pure/PIDE/batch_session.scala	Sat Mar 18 13:15:07 2017 +0100
+++ b/src/Pure/PIDE/batch_session.scala	Sat Mar 18 14:12:38 2017 +0100
@@ -47,10 +47,8 @@
           val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
           batch_session.build_theories_result =
             Some(Build.build_theories(prover_session, master_dir, theories))
-        case Session.Terminated(_) =>
-          batch_session.session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
-        case Session.Shutdown =>
-          batch_session.session_result.fulfill(())
+        case Session.Terminated(rc) =>
+          batch_session.session_result.fulfill(rc)
         case _ =>
       })
 
@@ -60,7 +58,7 @@
 
 class Batch_Session private(val session: Session)
 {
-  val session_result = Future.promise[Unit]
+  val session_result = Future.promise[Int]
   @volatile var build_theories_result: Option[Promise[XML.Body]] = None
 }