src/Pure/PIDE/protocol.scala
changeset 56352 abdc524db8b4
parent 56335 8953d4cc060a
child 56353 ecbdfe30bf7f
equal deleted inserted replaced
56351:1c735e46acf0 56352:abdc524db8b4
    39   }
    39   }
    40 
    40 
    41 
    41 
    42   /* command status */
    42   /* command status */
    43 
    43 
    44   object Status
       
    45   {
       
    46     val init = Status()
       
    47   }
       
    48 
       
    49   sealed case class Status(
    44   sealed case class Status(
    50     private val touched: Boolean = false,
    45     private val touched: Boolean,
    51     private val accepted: Boolean = false,
    46     private val accepted: Boolean,
    52     private val failed: Boolean = false,
    47     private val failed: Boolean,
    53     forks: Int = 0,
    48     forks: Int,
    54     runs: Int = 0)
    49     runs: Int)
    55   {
    50   {
    56     def + (that: Status): Status =
    51     def + (that: Status): Status =
    57       Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
    52       Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
    58         forks + that.forks, runs + that.runs)
    53         forks + that.forks, runs + that.runs)
    59 
    54 
    61     def is_running: Boolean = runs != 0
    56     def is_running: Boolean = runs != 0
    62     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    57     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    63     def is_failed: Boolean = failed
    58     def is_failed: Boolean = failed
    64   }
    59   }
    65 
    60 
    66   def command_status(status: Status, markup: Markup): Status =
    61   def command_status(markups: Iterator[Markup]): Status =
    67     markup match {
    62   {
    68       case Markup(Markup.ACCEPTED, _) => status.copy(accepted = true)
    63     var touched = false
    69       case Markup(Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1)
    64     var accepted = false
    70       case Markup(Markup.JOINED, _) => status.copy(forks = status.forks - 1)
    65     var failed = false
    71       case Markup(Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1)
    66     var forks = 0
    72       case Markup(Markup.FINISHED, _) => status.copy(runs = status.runs - 1)
    67     var runs = 0
    73       case Markup(Markup.FAILED, _) => status.copy(failed = true)
    68     for { markup <- markups; name = markup.name }
    74       case _ => status
    69       name match {
    75     }
    70         case Markup.ACCEPTED => accepted = true
    76 
    71         case Markup.FORKED => touched = true; forks += 1
    77   def command_status(status: Status, state: Command.State): Status =
    72         case Markup.JOINED => forks -= 1
    78     (status /: state.status)(command_status(_, _))
    73         case Markup.RUNNING => touched = true; runs += 1
    79 
    74         case Markup.FINISHED => runs -= 1
    80   def command_status(status: Status, states: List[Command.State]): Status =
    75         case Markup.FAILED => failed = true
    81     (status /: states)(command_status(_, _))
    76         case _ =>
       
    77       }
       
    78     Status(touched, accepted, failed, forks, runs)
       
    79   }
    82 
    80 
    83   val command_status_elements =
    81   val command_status_elements =
    84     Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    82     Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    85       Markup.FINISHED, Markup.FAILED)
    83       Markup.FINISHED, Markup.FAILED)
    86 
    84 
   121     var warned = 0
   119     var warned = 0
   122     var failed = 0
   120     var failed = 0
   123     for {
   121     for {
   124       command <- node.commands
   122       command <- node.commands
   125       states = state.command_states(version, command)
   123       states = state.command_states(version, command)
   126       status = command_status(Status.init, states)
   124       status = command_status(states.iterator.flatMap(st => st.status.iterator))
   127     } {
   125     } {
   128       if (status.is_running) running += 1
   126       if (status.is_running) running += 1
   129       else if (status.is_finished) {
   127       else if (status.is_finished) {
   130         val warning = states.exists(st => st.results.entries.exists(p => is_warning(p._2)))
   128         val warning = states.exists(st => st.results.entries.exists(p => is_warning(p._2)))
   131         if (warning) warned += 1 else finished += 1
   129         if (warning) warned += 1 else finished += 1