# HG changeset patch # User wenzelm # Date 1489871465 -3600 # Node ID b9f5cd8456167fb1d0f1ee61b3a3f8ba11cdfc53 # Parent c0fb8405416c38a3c078b113c14347c0590f71c0 more informative session result; diff -r c0fb8405416c -r b9f5cd845616 src/Pure/PIDE/markup.scala --- 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" diff -r c0fb8405416c -r b9f5cd845616 src/Pure/PIDE/prover.scala --- 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() } diff -r c0fb8405416c -r b9f5cd845616 src/Pure/PIDE/session.scala --- 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)) } } diff -r c0fb8405416c -r b9f5cd845616 src/Pure/System/bash.scala --- 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) } } } diff -r c0fb8405416c -r b9f5cd845616 src/Pure/Tools/build.scala --- 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 { diff -r c0fb8405416c -r b9f5cd845616 src/Tools/VSCode/src/server.scala --- 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 diff -r c0fb8405416c -r b9f5cd845616 src/Tools/jEdit/src/plugin.scala --- 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()))