more informative session result;

--- a/src/Pure/PIDE/markup.scala	Sat Mar 18 21:40:47 2017 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Mar 18 22:11:05 2017 +0100
@@ -368,6 +368,26 @@
   }
 
 
+  /* process result */
+
+  val Return_Code = new Properties.Int("return_code")
+
+  object Process_Result
+  {
+    def apply(result: Process_Result): Properties.T =
+      Return_Code(result.rc) :::
+        (if (result.timing.is_zero) Nil else Timing_Properties(result.timing))
+
+    def unapply(props: Properties.T): Option[Process_Result] =
+      props match {
+        case Return_Code(rc) =>
+          val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero)
+          Some(isabelle.Process_Result(rc, timing = timing))
+        case _ => None
+      }
+  }
+
+
   /* command timing */
 
   val COMMAND_TIMING = "command_timing"
@@ -451,8 +471,6 @@
 
   val message: String => String = messages.withDefault((s: String) => s)
 
-  val Return_Code = new Properties.Int("return_code")
-
   val NO_REPORT = "no_report"
 
   val BAD = "bad"

--- a/src/Pure/PIDE/prover.scala	Sat Mar 18 21:40:47 2017 +0100
+++ b/src/Pure/PIDE/prover.scala	Sat Mar 18 22:11:05 2017 +0100
@@ -89,17 +89,22 @@
     for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
   }
 
-  private def exit_message(rc: Int)
+  private def exit_message(result: Process_Result)
   {
-    output(Markup.EXIT, Markup.Return_Code(rc), List(XML.Text("Return code: " + rc.toString)))
+    output(Markup.EXIT, Markup.Process_Result(result),
+      List(XML.Text("Return code: " + result.rc.toString)))
   }
 
 
 
   /** process manager **/
 
-  private val process_result: Future[Int] =
-    Future.thread("process_result") { process.join }
+  private val process_result: Future[Process_Result] =
+    Future.thread("process_result") {
+      val rc = process.join
+      val timing = process.get_timing
+      Process_Result(rc, timing = timing)
+    }
 
   private def terminate_process()
   {
@@ -133,7 +138,7 @@
     if (startup_failed) {
       terminate_process()
       process_result.join
-      exit_message(127)
+      exit_message(Process_Result(127))
     }
     else {
       val (command_stream, message_stream) = channel.rendezvous()
@@ -143,12 +148,12 @@
       val stderr = physical_output(true)
       val message = message_output(message_stream)
 
-      val rc = process_result.join
+      val result = process_result.join
       system_output("process terminated")
       command_input_close()
       for (thread <- List(stdout, stderr, message)) thread.join
       system_output("process_manager terminated")
-      exit_message(rc)
+      exit_message(result)
     }
     channel.accepted()
   }

--- a/src/Pure/PIDE/session.scala	Sat Mar 18 21:40:47 2017 +0100
+++ b/src/Pure/PIDE/session.scala	Sat Mar 18 22:11:05 2017 +0100
@@ -71,7 +71,7 @@
   {
     def print: String =
       this match {
-        case Terminated(rc) => if (rc == 0) "finished" else "failed"
+        case Terminated(result) => if (result.ok) "finished" else "failed"
         case _ => Word.lowercase(this.toString)
       }
   }
@@ -79,7 +79,7 @@
   case object Startup extends Phase  // transient
   case object Ready extends Phase  // metastable
   case object Shutdown extends Phase  // transient
-  case class Terminated(rc: Int) extends Phase  // stable
+  case class Terminated(result: Process_Result) extends Phase  // stable
   //}}}
 
 
@@ -446,8 +446,8 @@
               phase = Session.Ready
               debugger.ready()
 
-            case Markup.Return_Code(rc) if output.is_exit =>
-              phase = Session.Terminated(rc)
+            case Markup.Process_Result(result) if output.is_exit =>
+              phase = Session.Terminated(result)
               prover.reset
 
             case _ =>
@@ -561,13 +561,13 @@
         phase match {
           case Session.Startup | Session.Shutdown => None
           case Session.Terminated(_) => Some((false, phase))
-          case Session.Inactive => Some((false, post_phase(Session.Terminated(0))))
+          case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0)))))
           case Session.Ready => Some((true, post_phase(Session.Shutdown)))
         })
     if (was_ready) manager.send(Stop)
   }
 
-  def stop(): Int =
+  def stop(): Process_Result =
   {
     send_stop()
     prover.await_reset()
@@ -578,7 +578,7 @@
     dispatcher.shutdown()
 
     phase match {
-      case Session.Terminated(rc) => rc
+      case Session.Terminated(result) => result
       case phase => error("Bad session phase after shutdown: " + quote(phase.print))
     }
   }

--- a/src/Pure/System/bash.scala	Sat Mar 18 21:40:47 2017 +0100
+++ b/src/Pure/System/bash.scala	Sat Mar 18 22:11:05 2017 +0100
@@ -72,6 +72,7 @@
   {
     private val timing_file = Isabelle_System.tmp_file("bash_timing")
     private val timing = Synchronized[Option[Timing]](None)
+    def get_timing: Timing = timing.value getOrElse Timing.zero
 
     private val script_file = Isabelle_System.tmp_file("bash_script")
     File.write(script_file, script)
@@ -199,7 +200,7 @@
         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
-      Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero)
+      Process_Result(rc, out_lines.join, err_lines.join, false, get_timing)
     }
   }
 }

--- a/src/Pure/Tools/build.scala	Sat Mar 18 21:40:47 2017 +0100
+++ b/src/Pure/Tools/build.scala	Sat Mar 18 22:11:05 2017 +0100
@@ -225,22 +225,24 @@
           val handler = new Handler(progress, session, name)
           session.init_protocol_handler(handler)
 
-          val session_result = Future.promise[Int]
+          val session_result = Future.promise[Process_Result]
 
           Isabelle_Process.start(session, options, logic = parent,
             cwd = info.dir.file, env = env, tree = Some(tree), store = store,
             phase_changed =
             {
               case Session.Ready => session.protocol_command("build_session", args_yxml)
-              case Session.Terminated(rc) => session_result.fulfill(rc)
+              case Session.Terminated(result) => session_result.fulfill(result)
               case _ =>
             })
 
-          val rc = session_result.join
-
+          val result = session_result.join
           handler.result_error.join match {
-            case "" => Process_Result(rc)
-            case msg => Process_Result(rc max 1, out_lines = split_lines(Output.error_text(msg)))
+            case "" => result
+            case msg =>
+              result.copy(
+                rc = result.rc max 1,
+                out_lines = result.out_lines ::: split_lines(Output.error_text(msg)))
           }
         }
         else {

--- a/src/Tools/VSCode/src/server.scala	Sat Mar 18 21:40:47 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sat Mar 18 22:11:05 2017 +0100
@@ -252,9 +252,9 @@
           case Session.Ready =>
             session.phase_changed -= session_phase
             reply("")
-          case Session.Terminated(rc) if rc != 0 =>
+          case Session.Terminated(result) if !result.ok =>
             session.phase_changed -= session_phase
-            reply("Prover startup failed: return code " + rc)
+            reply("Prover startup failed: return code " + result.rc)
           case _ =>
         }
       session.phase_changed += session_phase

--- a/src/Tools/jEdit/src/plugin.scala	Sat Mar 18 21:40:47 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Mar 18 22:11:05 2017 +0100
@@ -191,7 +191,7 @@
 
   val session_phase_changed: Session.Phase => Unit =
   {
-    case Session.Terminated(rc) if rc != 0 =>
+    case Session.Terminated(result) if !result.ok =>
       GUI_Thread.later {
         GUI.error_dialog(jEdit.getActiveView, "Prover process terminated with error",
           "Isabelle Syslog", GUI.scrollable_text(session.syslog_content()))