src/Pure/PIDE/protocol.scala
changeset 68758 a110e7e24e55
parent 68381 2fd3a6d6ba2e
child 69846 e02e3763e7a4
equal deleted inserted replaced
68757:e7e3776385ba 68758:a110e7e24e55
    34       catch {
    34       catch {
    35         case ERROR(_) => None
    35         case ERROR(_) => None
    36         case _: XML.Error => None
    36         case _: XML.Error => None
    37       }
    37       }
    38   }
    38   }
    39 
       
    40 
       
    41   /* consolidation status */
       
    42 
       
    43   def maybe_consolidated(markups: List[Markup]): Boolean =
       
    44   {
       
    45     var touched = false
       
    46     var forks = 0
       
    47     var runs = 0
       
    48     for (markup <- markups) {
       
    49       markup.name match {
       
    50         case Markup.FORKED => touched = true; forks += 1
       
    51         case Markup.JOINED => forks -= 1
       
    52         case Markup.RUNNING => touched = true; runs += 1
       
    53         case Markup.FINISHED => runs -= 1
       
    54         case _ =>
       
    55       }
       
    56     }
       
    57     touched && forks == 0 && runs == 0
       
    58   }
       
    59 
       
    60 
       
    61   /* command status */
       
    62 
       
    63   object Status
       
    64   {
       
    65     def make(markup_iterator: Iterator[Markup]): Status =
       
    66     {
       
    67       var touched = false
       
    68       var accepted = false
       
    69       var warned = false
       
    70       var failed = false
       
    71       var forks = 0
       
    72       var runs = 0
       
    73       for (markup <- markup_iterator) {
       
    74         markup.name match {
       
    75           case Markup.ACCEPTED => accepted = true
       
    76           case Markup.FORKED => touched = true; forks += 1
       
    77           case Markup.JOINED => forks -= 1
       
    78           case Markup.RUNNING => touched = true; runs += 1
       
    79           case Markup.FINISHED => runs -= 1
       
    80           case Markup.WARNING | Markup.LEGACY => warned = true
       
    81           case Markup.FAILED | Markup.ERROR => failed = true
       
    82           case _ =>
       
    83         }
       
    84       }
       
    85       Status(touched, accepted, warned, failed, forks, runs)
       
    86     }
       
    87 
       
    88     val empty = make(Iterator.empty)
       
    89 
       
    90     def merge(status_iterator: Iterator[Status]): Status =
       
    91       if (status_iterator.hasNext) {
       
    92         val status0 = status_iterator.next
       
    93         (status0 /: status_iterator)(_ + _)
       
    94       }
       
    95       else empty
       
    96   }
       
    97 
       
    98   sealed case class Status(
       
    99     private val touched: Boolean,
       
   100     private val accepted: Boolean,
       
   101     private val warned: Boolean,
       
   102     private val failed: Boolean,
       
   103     forks: Int,
       
   104     runs: Int)
       
   105   {
       
   106     def + (that: Status): Status =
       
   107       Status(
       
   108         touched || that.touched,
       
   109         accepted || that.accepted,
       
   110         warned || that.warned,
       
   111         failed || that.failed,
       
   112         forks + that.forks,
       
   113         runs + that.runs)
       
   114 
       
   115     def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
       
   116     def is_running: Boolean = runs != 0
       
   117     def is_warned: Boolean = warned
       
   118     def is_failed: Boolean = failed
       
   119     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
       
   120   }
       
   121 
       
   122   val proper_status_elements =
       
   123     Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
       
   124       Markup.FINISHED, Markup.FAILED)
       
   125 
       
   126   val liberal_status_elements =
       
   127     proper_status_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
       
   128 
    39 
   129 
    40 
   130   /* command timing */
    41   /* command timing */
   131 
    42 
   132   object Command_Timing
    43   object Command_Timing
   154             case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing))
    65             case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing))
   155             case _ => None
    66             case _ => None
   156           }
    67           }
   157         case _ => None
    68         case _ => None
   158       }
    69       }
   159   }
       
   160 
       
   161 
       
   162   /* node status */
       
   163 
       
   164   sealed case class Node_Status(
       
   165     unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
       
   166     initialized: Boolean, consolidated: Boolean)
       
   167   {
       
   168     def ok: Boolean = failed == 0
       
   169     def total: Int = unprocessed + running + warned + failed + finished
       
   170 
       
   171     def json: JSON.Object.T =
       
   172       JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
       
   173         "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
       
   174         "initialized" -> initialized, "consolidated" -> consolidated)
       
   175   }
       
   176 
       
   177   def node_status(
       
   178     state: Document.State,
       
   179     version: Document.Version,
       
   180     name: Document.Node.Name): Node_Status =
       
   181   {
       
   182     val node = version.nodes(name)
       
   183 
       
   184     var unprocessed = 0
       
   185     var running = 0
       
   186     var warned = 0
       
   187     var failed = 0
       
   188     var finished = 0
       
   189     for (command <- node.commands.iterator) {
       
   190       val states = state.command_states(version, command)
       
   191       val status = Status.merge(states.iterator.map(_.protocol_status))
       
   192 
       
   193       if (status.is_running) running += 1
       
   194       else if (status.is_failed) failed += 1
       
   195       else if (status.is_warned) warned += 1
       
   196       else if (status.is_finished) finished += 1
       
   197       else unprocessed += 1
       
   198     }
       
   199     val initialized = state.node_initialized(version, name)
       
   200     val consolidated = state.node_consolidated(version, name)
       
   201 
       
   202     Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated)
       
   203   }
       
   204 
       
   205 
       
   206   /* node timing */
       
   207 
       
   208   sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
       
   209 
       
   210   val empty_node_timing = Node_Timing(0.0, Map.empty)
       
   211 
       
   212   def node_timing(
       
   213     state: Document.State,
       
   214     version: Document.Version,
       
   215     node: Document.Node,
       
   216     threshold: Double): Node_Timing =
       
   217   {
       
   218     var total = 0.0
       
   219     var commands = Map.empty[Command, Double]
       
   220     for {
       
   221       command <- node.commands.iterator
       
   222       st <- state.command_states(version, command)
       
   223     } {
       
   224       val command_timing =
       
   225         (0.0 /: st.status)({
       
   226           case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
       
   227           case (timing, _) => timing
       
   228         })
       
   229       total += command_timing
       
   230       if (command_timing >= threshold) commands += (command -> command_timing)
       
   231     }
       
   232     Node_Timing(total, commands)
       
   233   }
    70   }
   234 
    71 
   235 
    72 
   236   /* result messages */
    73   /* result messages */
   237 
    74