src/Pure/PIDE/markup.scala
changeset 65317 b9f5cd845616
parent 65313 347ed6219dab
child 65335 7634d33c1a79
     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"