more informative session result;
authorwenzelm
Sat Mar 18 22:11:05 2017 +0100 (2017-03-18 ago)
changeset 65317b9f5cd845616
parent 65316 c0fb8405416c
child 65318 342efc382558
more informative session result;
src/Pure/PIDE/markup.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/session.scala
src/Pure/System/bash.scala
src/Pure/Tools/build.scala
src/Tools/VSCode/src/server.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Sat Mar 18 21:40:47 2017 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sat Mar 18 22:11:05 2017 +0100
     1.3 @@ -368,6 +368,26 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* process result */
     1.8 +
     1.9 +  val Return_Code = new Properties.Int("return_code")
    1.10 +
    1.11 +  object Process_Result
    1.12 +  {
    1.13 +    def apply(result: Process_Result): Properties.T =
    1.14 +      Return_Code(result.rc) :::
    1.15 +        (if (result.timing.is_zero) Nil else Timing_Properties(result.timing))
    1.16 +
    1.17 +    def unapply(props: Properties.T): Option[Process_Result] =
    1.18 +      props match {
    1.19 +        case Return_Code(rc) =>
    1.20 +          val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero)
    1.21 +          Some(isabelle.Process_Result(rc, timing = timing))
    1.22 +        case _ => None
    1.23 +      }
    1.24 +  }
    1.25 +
    1.26 +
    1.27    /* command timing */
    1.28  
    1.29    val COMMAND_TIMING = "command_timing"
    1.30 @@ -451,8 +471,6 @@
    1.31  
    1.32    val message: String => String = messages.withDefault((s: String) => s)
    1.33  
    1.34 -  val Return_Code = new Properties.Int("return_code")
    1.35 -
    1.36    val NO_REPORT = "no_report"
    1.37  
    1.38    val BAD = "bad"
     2.1 --- a/src/Pure/PIDE/prover.scala	Sat Mar 18 21:40:47 2017 +0100
     2.2 +++ b/src/Pure/PIDE/prover.scala	Sat Mar 18 22:11:05 2017 +0100
     2.3 @@ -89,17 +89,22 @@
     2.4      for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
     2.5    }
     2.6  
     2.7 -  private def exit_message(rc: Int)
     2.8 +  private def exit_message(result: Process_Result)
     2.9    {
    2.10 -    output(Markup.EXIT, Markup.Return_Code(rc), List(XML.Text("Return code: " + rc.toString)))
    2.11 +    output(Markup.EXIT, Markup.Process_Result(result),
    2.12 +      List(XML.Text("Return code: " + result.rc.toString)))
    2.13    }
    2.14  
    2.15  
    2.16  
    2.17    /** process manager **/
    2.18  
    2.19 -  private val process_result: Future[Int] =
    2.20 -    Future.thread("process_result") { process.join }
    2.21 +  private val process_result: Future[Process_Result] =
    2.22 +    Future.thread("process_result") {
    2.23 +      val rc = process.join
    2.24 +      val timing = process.get_timing
    2.25 +      Process_Result(rc, timing = timing)
    2.26 +    }
    2.27  
    2.28    private def terminate_process()
    2.29    {
    2.30 @@ -133,7 +138,7 @@
    2.31      if (startup_failed) {
    2.32        terminate_process()
    2.33        process_result.join
    2.34 -      exit_message(127)
    2.35 +      exit_message(Process_Result(127))
    2.36      }
    2.37      else {
    2.38        val (command_stream, message_stream) = channel.rendezvous()
    2.39 @@ -143,12 +148,12 @@
    2.40        val stderr = physical_output(true)
    2.41        val message = message_output(message_stream)
    2.42  
    2.43 -      val rc = process_result.join
    2.44 +      val result = process_result.join
    2.45        system_output("process terminated")
    2.46        command_input_close()
    2.47        for (thread <- List(stdout, stderr, message)) thread.join
    2.48        system_output("process_manager terminated")
    2.49 -      exit_message(rc)
    2.50 +      exit_message(result)
    2.51      }
    2.52      channel.accepted()
    2.53    }
     3.1 --- a/src/Pure/PIDE/session.scala	Sat Mar 18 21:40:47 2017 +0100
     3.2 +++ b/src/Pure/PIDE/session.scala	Sat Mar 18 22:11:05 2017 +0100
     3.3 @@ -71,7 +71,7 @@
     3.4    {
     3.5      def print: String =
     3.6        this match {
     3.7 -        case Terminated(rc) => if (rc == 0) "finished" else "failed"
     3.8 +        case Terminated(result) => if (result.ok) "finished" else "failed"
     3.9          case _ => Word.lowercase(this.toString)
    3.10        }
    3.11    }
    3.12 @@ -79,7 +79,7 @@
    3.13    case object Startup extends Phase  // transient
    3.14    case object Ready extends Phase  // metastable
    3.15    case object Shutdown extends Phase  // transient
    3.16 -  case class Terminated(rc: Int) extends Phase  // stable
    3.17 +  case class Terminated(result: Process_Result) extends Phase  // stable
    3.18    //}}}
    3.19  
    3.20  
    3.21 @@ -446,8 +446,8 @@
    3.22                phase = Session.Ready
    3.23                debugger.ready()
    3.24  
    3.25 -            case Markup.Return_Code(rc) if output.is_exit =>
    3.26 -              phase = Session.Terminated(rc)
    3.27 +            case Markup.Process_Result(result) if output.is_exit =>
    3.28 +              phase = Session.Terminated(result)
    3.29                prover.reset
    3.30  
    3.31              case _ =>
    3.32 @@ -561,13 +561,13 @@
    3.33          phase match {
    3.34            case Session.Startup | Session.Shutdown => None
    3.35            case Session.Terminated(_) => Some((false, phase))
    3.36 -          case Session.Inactive => Some((false, post_phase(Session.Terminated(0))))
    3.37 +          case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0)))))
    3.38            case Session.Ready => Some((true, post_phase(Session.Shutdown)))
    3.39          })
    3.40      if (was_ready) manager.send(Stop)
    3.41    }
    3.42  
    3.43 -  def stop(): Int =
    3.44 +  def stop(): Process_Result =
    3.45    {
    3.46      send_stop()
    3.47      prover.await_reset()
    3.48 @@ -578,7 +578,7 @@
    3.49      dispatcher.shutdown()
    3.50  
    3.51      phase match {
    3.52 -      case Session.Terminated(rc) => rc
    3.53 +      case Session.Terminated(result) => result
    3.54        case phase => error("Bad session phase after shutdown: " + quote(phase.print))
    3.55      }
    3.56    }
     4.1 --- a/src/Pure/System/bash.scala	Sat Mar 18 21:40:47 2017 +0100
     4.2 +++ b/src/Pure/System/bash.scala	Sat Mar 18 22:11:05 2017 +0100
     4.3 @@ -72,6 +72,7 @@
     4.4    {
     4.5      private val timing_file = Isabelle_System.tmp_file("bash_timing")
     4.6      private val timing = Synchronized[Option[Timing]](None)
     4.7 +    def get_timing: Timing = timing.value getOrElse Timing.zero
     4.8  
     4.9      private val script_file = Isabelle_System.tmp_file("bash_script")
    4.10      File.write(script_file, script)
    4.11 @@ -199,7 +200,7 @@
    4.12          catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
    4.13        if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
    4.14  
    4.15 -      Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero)
    4.16 +      Process_Result(rc, out_lines.join, err_lines.join, false, get_timing)
    4.17      }
    4.18    }
    4.19  }
     5.1 --- a/src/Pure/Tools/build.scala	Sat Mar 18 21:40:47 2017 +0100
     5.2 +++ b/src/Pure/Tools/build.scala	Sat Mar 18 22:11:05 2017 +0100
     5.3 @@ -225,22 +225,24 @@
     5.4            val handler = new Handler(progress, session, name)
     5.5            session.init_protocol_handler(handler)
     5.6  
     5.7 -          val session_result = Future.promise[Int]
     5.8 +          val session_result = Future.promise[Process_Result]
     5.9  
    5.10            Isabelle_Process.start(session, options, logic = parent,
    5.11              cwd = info.dir.file, env = env, tree = Some(tree), store = store,
    5.12              phase_changed =
    5.13              {
    5.14                case Session.Ready => session.protocol_command("build_session", args_yxml)
    5.15 -              case Session.Terminated(rc) => session_result.fulfill(rc)
    5.16 +              case Session.Terminated(result) => session_result.fulfill(result)
    5.17                case _ =>
    5.18              })
    5.19  
    5.20 -          val rc = session_result.join
    5.21 -
    5.22 +          val result = session_result.join
    5.23            handler.result_error.join match {
    5.24 -            case "" => Process_Result(rc)
    5.25 -            case msg => Process_Result(rc max 1, out_lines = split_lines(Output.error_text(msg)))
    5.26 +            case "" => result
    5.27 +            case msg =>
    5.28 +              result.copy(
    5.29 +                rc = result.rc max 1,
    5.30 +                out_lines = result.out_lines ::: split_lines(Output.error_text(msg)))
    5.31            }
    5.32          }
    5.33          else {
     6.1 --- a/src/Tools/VSCode/src/server.scala	Sat Mar 18 21:40:47 2017 +0100
     6.2 +++ b/src/Tools/VSCode/src/server.scala	Sat Mar 18 22:11:05 2017 +0100
     6.3 @@ -252,9 +252,9 @@
     6.4            case Session.Ready =>
     6.5              session.phase_changed -= session_phase
     6.6              reply("")
     6.7 -          case Session.Terminated(rc) if rc != 0 =>
     6.8 +          case Session.Terminated(result) if !result.ok =>
     6.9              session.phase_changed -= session_phase
    6.10 -            reply("Prover startup failed: return code " + rc)
    6.11 +            reply("Prover startup failed: return code " + result.rc)
    6.12            case _ =>
    6.13          }
    6.14        session.phase_changed += session_phase
     7.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Mar 18 21:40:47 2017 +0100
     7.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Mar 18 22:11:05 2017 +0100
     7.3 @@ -191,7 +191,7 @@
     7.4  
     7.5    val session_phase_changed: Session.Phase => Unit =
     7.6    {
     7.7 -    case Session.Terminated(rc) if rc != 0 =>
     7.8 +    case Session.Terminated(result) if !result.ok =>
     7.9        GUI_Thread.later {
    7.10          GUI.error_dialog(jEdit.getActiveView, "Prover process terminated with error",
    7.11            "Isabelle Syslog", GUI.scrollable_text(session.syslog_content()))