src/Pure/Tools/build_log.scala
changeset 64086 ac7ae5067783
parent 64085 1c451e5c145f
child 64087 a77c57235bae
     1.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 17:12:47 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 17:41:19 2016 +0200
     1.3 @@ -249,7 +249,6 @@
     1.4      ml_timing: Option[Timing],
     1.5      status: Session_Status.Value)
     1.6    {
     1.7 -    def ok: Boolean = status == Session_Status.EXISTING || status == Session_Status.FINISHED
     1.8      def finished: Boolean = status == Session_Status.FINISHED
     1.9    }
    1.10  
    1.11 @@ -290,6 +289,7 @@
    1.12        new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
    1.13      val Session_Timing =
    1.14        new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
    1.15 +    val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
    1.16      val Session_Failed = new Regex("""^(\S+) FAILED""")
    1.17      val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
    1.18  
    1.19 @@ -298,11 +298,12 @@
    1.20      var threads = Map.empty[String, Int]
    1.21      var timing = Map.empty[String, Timing]
    1.22      var ml_timing = Map.empty[String, Timing]
    1.23 +    var started = Set.empty[String]
    1.24      var failed = Set.empty[String]
    1.25      var cancelled = Set.empty[String]
    1.26      def all_sessions: Set[String] =
    1.27        chapter.keySet ++ groups.keySet ++ threads.keySet ++
    1.28 -      timing.keySet ++ ml_timing.keySet ++ failed ++ cancelled
    1.29 +      timing.keySet ++ ml_timing.keySet ++ failed ++ cancelled ++ started
    1.30  
    1.31  
    1.32      for (line <- log_file.lines) {
    1.33 @@ -313,6 +314,8 @@
    1.34          case Session_Groups(Chapter_Name(chapt, name), grps) =>
    1.35            chapter += (name -> chapt)
    1.36            groups += (name -> Word.explode(grps))
    1.37 +        case Session_Started(name) =>
    1.38 +          started += name
    1.39          case Session_Finished1(name,
    1.40              Value.Int(e1), Value.Int(e2), Value.Int(e3),
    1.41              Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
    1.42 @@ -340,7 +343,9 @@
    1.43            val status =
    1.44              if (failed(name)) Session_Status.FAILED
    1.45              else if (cancelled(name)) Session_Status.CANCELLED
    1.46 -            else if (timing.isDefinedAt(name)) Session_Status.FINISHED
    1.47 +            else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
    1.48 +              Session_Status.FINISHED
    1.49 +            else if (started(name)) Session_Status.FAILED
    1.50              else Session_Status.EXISTING
    1.51            val entry =
    1.52              Session_Entry(