src/Pure/PIDE/document_status.scala
author wenzelm
Mon Sep 03 15:04:04 2018 +0200 (10 months ago)
changeset 68892 dce6cbd3cafc
parent 68889 d9c051e9da2b
child 68897 bdc38f0fd68c
permissions -rw-r--r--
proper polarity of terminated status;
     1 /*  Title:      Pure/PIDE/document_status.scala
     2     Author:     Makarius
     3 
     4 Document status based on markup information.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Document_Status
    11 {
    12   /* command status */
    13 
    14   object Command_Status
    15   {
    16     val proper_elements: Markup.Elements =
    17       Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    18         Markup.FINISHED, Markup.FAILED, Markup.CANCELED)
    19 
    20     val liberal_elements: Markup.Elements =
    21       proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
    22 
    23     def make(markup_iterator: Iterator[Markup]): Command_Status =
    24     {
    25       var touched = false
    26       var accepted = false
    27       var warned = false
    28       var failed = false
    29       var canceled = false
    30       var finalized = false
    31       var forks = 0
    32       var runs = 0
    33       for (markup <- markup_iterator) {
    34         markup.name match {
    35           case Markup.ACCEPTED => accepted = true
    36           case Markup.FORKED => touched = true; forks += 1
    37           case Markup.JOINED => forks -= 1
    38           case Markup.RUNNING => touched = true; runs += 1
    39           case Markup.FINISHED => runs -= 1
    40           case Markup.WARNING | Markup.LEGACY => warned = true
    41           case Markup.FAILED | Markup.ERROR => failed = true
    42           case Markup.CANCELED => canceled = true
    43           case Markup.FINALIZED => finalized = true
    44           case _ =>
    45         }
    46       }
    47       Command_Status(
    48         touched = touched,
    49         accepted = accepted,
    50         warned = warned,
    51         failed = failed,
    52         canceled = canceled,
    53         finalized = finalized,
    54         forks = forks,
    55         runs = runs)
    56     }
    57 
    58     val empty = make(Iterator.empty)
    59 
    60     def merge(status_iterator: Iterator[Command_Status]): Command_Status =
    61       if (status_iterator.hasNext) {
    62         val status0 = status_iterator.next
    63         (status0 /: status_iterator)(_ + _)
    64       }
    65       else empty
    66   }
    67 
    68   sealed case class Command_Status(
    69     private val touched: Boolean,
    70     private val accepted: Boolean,
    71     private val warned: Boolean,
    72     private val failed: Boolean,
    73     private val canceled: Boolean,
    74     private val finalized: Boolean,
    75     forks: Int,
    76     runs: Int)
    77   {
    78     def + (that: Command_Status): Command_Status =
    79       Command_Status(
    80         touched = touched || that.touched,
    81         accepted = accepted || that.accepted,
    82         warned = warned || that.warned,
    83         failed = failed || that.failed,
    84         canceled = canceled || that.canceled,
    85         finalized = finalized || that.finalized,
    86         forks = forks + that.forks,
    87         runs = runs + that.runs)
    88 
    89     def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
    90     def is_running: Boolean = runs != 0
    91     def is_warned: Boolean = warned
    92     def is_failed: Boolean = failed
    93     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    94     def is_canceled: Boolean = canceled
    95     def is_finalized: Boolean = finalized
    96     def is_terminated: Boolean = canceled || touched && forks == 0 && runs == 0
    97   }
    98 
    99 
   100   /* node status */
   101 
   102   object Node_Status
   103   {
   104     def make(
   105       state: Document.State,
   106       version: Document.Version,
   107       name: Document.Node.Name): Node_Status =
   108     {
   109       val node = version.nodes(name)
   110 
   111       var unprocessed = 0
   112       var running = 0
   113       var warned = 0
   114       var failed = 0
   115       var finished = 0
   116       var canceled = false
   117       var terminated = true
   118       var finalized = false
   119       for (command <- node.commands.iterator) {
   120         val states = state.command_states(version, command)
   121         val status = Command_Status.merge(states.iterator.map(_.document_status))
   122 
   123         if (status.is_running) running += 1
   124         else if (status.is_failed) failed += 1
   125         else if (status.is_warned) warned += 1
   126         else if (status.is_finished) finished += 1
   127         else unprocessed += 1
   128 
   129         if (status.is_canceled) canceled = true
   130         if (!status.is_terminated) terminated = false
   131         if (status.is_finalized) finalized = true
   132       }
   133       val initialized = state.node_initialized(version, name)
   134       val consolidated = state.node_consolidated(version, name)
   135 
   136       Node_Status(
   137         unprocessed = unprocessed,
   138         running = running,
   139         warned = warned,
   140         failed = failed,
   141         finished = finished,
   142         canceled = canceled,
   143         terminated = terminated,
   144         initialized = initialized,
   145         finalized = finalized,
   146         consolidated = consolidated)
   147     }
   148   }
   149 
   150   sealed case class Node_Status(
   151     unprocessed: Int,
   152     running: Int,
   153     warned: Int,
   154     failed: Int,
   155     finished: Int,
   156     canceled: Boolean,
   157     terminated: Boolean,
   158     initialized: Boolean,
   159     finalized: Boolean,
   160     consolidated: Boolean)
   161   {
   162     def ok: Boolean = failed == 0
   163     def total: Int = unprocessed + running + warned + failed + finished
   164 
   165     def json: JSON.Object.T =
   166       JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
   167         "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
   168         "canceled" -> canceled, "consolidated" -> consolidated)
   169   }
   170 
   171 
   172   /* node timing */
   173 
   174   object Node_Timing
   175   {
   176     val empty: Node_Timing = Node_Timing(0.0, Map.empty)
   177 
   178     def make(
   179       state: Document.State,
   180       version: Document.Version,
   181       node: Document.Node,
   182       threshold: Double): Node_Timing =
   183     {
   184       var total = 0.0
   185       var commands = Map.empty[Command, Double]
   186       for {
   187         command <- node.commands.iterator
   188         st <- state.command_states(version, command)
   189       } {
   190         val command_timing =
   191           (0.0 /: st.status)({
   192             case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
   193             case (timing, _) => timing
   194           })
   195         total += command_timing
   196         if (command_timing >= threshold) commands += (command -> command_timing)
   197       }
   198       Node_Timing(total, commands)
   199     }
   200   }
   201 
   202   sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
   203 
   204 
   205   /* nodes status */
   206 
   207   object Overall_Node_Status extends Enumeration
   208   {
   209     val ok, failed, pending = Value
   210   }
   211 
   212   object Nodes_Status
   213   {
   214     val empty: Nodes_Status = new Nodes_Status(Map.empty)
   215 
   216     type Update = (Nodes_Status, List[Document.Node.Name])
   217     val empty_update: Update = (empty, Nil)
   218   }
   219 
   220   final class Nodes_Status private(private val rep: Map[Document.Node.Name, Node_Status])
   221   {
   222     def is_empty: Boolean = rep.isEmpty
   223     def apply(name: Document.Node.Name): Node_Status = rep(name)
   224     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
   225 
   226     def quasi_consolidated(name: Document.Node.Name): Boolean =
   227       rep.get(name) match {
   228         case Some(st) => !st.finalized && st.terminated
   229         case None => false
   230       }
   231 
   232     def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
   233       rep.get(name) match {
   234         case Some(st) if st.consolidated =>
   235           if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
   236         case _ => Overall_Node_Status.pending
   237       }
   238 
   239     def update(
   240       session_base: Sessions.Base,
   241       state: Document.State,
   242       version: Document.Version,
   243       domain: Option[Set[Document.Node.Name]] = None,
   244       trim: Boolean = false): Option[Nodes_Status.Update] =
   245     {
   246       val nodes = version.nodes
   247       val update_iterator =
   248         for {
   249           name <- domain.getOrElse(nodes.domain).iterator
   250           if !Sessions.is_hidden(name) &&
   251               !session_base.loaded_theory(name) &&
   252               !nodes.is_suppressed(name) &&
   253               !nodes(name).is_empty
   254           st = Document_Status.Node_Status.make(state, version, name)
   255           if !rep.isDefinedAt(name) || rep(name) != st
   256         } yield (name -> st)
   257       val rep1 = rep ++ update_iterator
   258       val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes.domain) else rep1
   259 
   260       if (rep == rep2) None
   261       else Some(new Nodes_Status(rep2), version.nodes.topological_order.filter(rep2.keySet))
   262     }
   263 
   264     override def hashCode: Int = rep.hashCode
   265     override def equals(that: Any): Boolean =
   266       that match {
   267         case other: Nodes_Status => rep == other.rep
   268         case _ => false
   269       }
   270 
   271     override def toString: String =
   272     {
   273       var ok = 0
   274       var failed = 0
   275       var pending = 0
   276       var canceled = 0
   277       for (name <- rep.keysIterator) {
   278         overall_node_status(name) match {
   279           case Overall_Node_Status.ok => ok += 1
   280           case Overall_Node_Status.failed => failed += 1
   281           case Overall_Node_Status.pending => pending += 1
   282         }
   283         if (apply(name).canceled) canceled += 1
   284       }
   285       "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending +
   286         ", canceled = " + canceled + ")"
   287     }
   288   }
   289 }