src/Pure/PIDE/document_status.scala
author wenzelm
Sat Sep 01 23:30:44 2018 +0200 (12 months ago)
changeset 68873 13a984eba612
parent 68871 f5c76072db55
child 68881 d975449b266e
permissions -rw-r--r--
clarified message;
     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 forks = 0
    31       var runs = 0
    32       for (markup <- markup_iterator) {
    33         markup.name match {
    34           case Markup.ACCEPTED => accepted = true
    35           case Markup.FORKED => touched = true; forks += 1
    36           case Markup.JOINED => forks -= 1
    37           case Markup.RUNNING => touched = true; runs += 1
    38           case Markup.FINISHED => runs -= 1
    39           case Markup.WARNING | Markup.LEGACY => warned = true
    40           case Markup.FAILED | Markup.ERROR => failed = true
    41           case Markup.CANCELED => canceled = true
    42           case _ =>
    43         }
    44       }
    45       Command_Status(touched, accepted, warned, failed, canceled, forks, runs)
    46     }
    47 
    48     val empty = make(Iterator.empty)
    49 
    50     def merge(status_iterator: Iterator[Command_Status]): Command_Status =
    51       if (status_iterator.hasNext) {
    52         val status0 = status_iterator.next
    53         (status0 /: status_iterator)(_ + _)
    54       }
    55       else empty
    56   }
    57 
    58   sealed case class Command_Status(
    59     private val touched: Boolean,
    60     private val accepted: Boolean,
    61     private val warned: Boolean,
    62     private val failed: Boolean,
    63     private val canceled: Boolean,
    64     forks: Int,
    65     runs: Int)
    66   {
    67     def + (that: Command_Status): Command_Status =
    68       Command_Status(
    69         touched || that.touched,
    70         accepted || that.accepted,
    71         warned || that.warned,
    72         failed || that.failed,
    73         canceled || that.canceled,
    74         forks + that.forks,
    75         runs + that.runs)
    76 
    77     def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
    78     def is_running: Boolean = runs != 0
    79     def is_warned: Boolean = warned
    80     def is_failed: Boolean = failed
    81     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    82     def is_canceled: Boolean = canceled
    83   }
    84 
    85 
    86   /* node status */
    87 
    88   object Node_Status
    89   {
    90     def make(
    91       state: Document.State,
    92       version: Document.Version,
    93       name: Document.Node.Name): Node_Status =
    94     {
    95       val node = version.nodes(name)
    96 
    97       var unprocessed = 0
    98       var running = 0
    99       var warned = 0
   100       var failed = 0
   101       var finished = 0
   102       var canceled = false
   103       for (command <- node.commands.iterator) {
   104         val states = state.command_states(version, command)
   105         val status = Command_Status.merge(states.iterator.map(_.document_status))
   106 
   107         if (status.is_running) running += 1
   108         else if (status.is_failed) failed += 1
   109         else if (status.is_warned) warned += 1
   110         else if (status.is_finished) finished += 1
   111         else unprocessed += 1
   112 
   113         if (status.is_canceled) canceled = true
   114       }
   115       val initialized = state.node_initialized(version, name)
   116       val consolidated = state.node_consolidated(version, name)
   117 
   118       Node_Status(
   119         unprocessed, running, warned, failed, finished, canceled, initialized, consolidated)
   120     }
   121   }
   122 
   123   sealed case class Node_Status(
   124     unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
   125     canceled: Boolean, initialized: Boolean, consolidated: Boolean)
   126   {
   127     def ok: Boolean = failed == 0
   128     def total: Int = unprocessed + running + warned + failed + finished
   129 
   130     def json: JSON.Object.T =
   131       JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
   132         "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
   133         "canceled" -> canceled, "initialized" -> initialized, "consolidated" -> consolidated)
   134   }
   135 
   136 
   137   /* node timing */
   138 
   139   object Node_Timing
   140   {
   141     val empty: Node_Timing = Node_Timing(0.0, Map.empty)
   142 
   143     def make(
   144       state: Document.State,
   145       version: Document.Version,
   146       node: Document.Node,
   147       threshold: Double): Node_Timing =
   148     {
   149       var total = 0.0
   150       var commands = Map.empty[Command, Double]
   151       for {
   152         command <- node.commands.iterator
   153         st <- state.command_states(version, command)
   154       } {
   155         val command_timing =
   156           (0.0 /: st.status)({
   157             case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
   158             case (timing, _) => timing
   159           })
   160         total += command_timing
   161         if (command_timing >= threshold) commands += (command -> command_timing)
   162       }
   163       Node_Timing(total, commands)
   164     }
   165   }
   166 
   167   sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
   168 
   169 
   170   /* nodes status */
   171 
   172   object Overall_Node_Status extends Enumeration
   173   {
   174     val ok, failed, pending = Value
   175   }
   176 
   177   object Nodes_Status
   178   {
   179     val empty: Nodes_Status = new Nodes_Status(Map.empty)
   180 
   181     type Update = (Nodes_Status, List[Document.Node.Name])
   182     val empty_update: Update = (empty, Nil)
   183   }
   184 
   185   final class Nodes_Status private(private val rep: Map[Document.Node.Name, Node_Status])
   186   {
   187     def is_empty: Boolean = rep.isEmpty
   188     def apply(name: Document.Node.Name): Node_Status = rep(name)
   189     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
   190 
   191     def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
   192       rep.get(name) match {
   193         case Some(st) if st.consolidated =>
   194           if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
   195         case _ => Overall_Node_Status.pending
   196       }
   197 
   198     def update(
   199       session_base: Sessions.Base,
   200       state: Document.State,
   201       version: Document.Version,
   202       domain: Option[Set[Document.Node.Name]] = None,
   203       trim: Boolean = false): Option[Nodes_Status.Update] =
   204     {
   205       val nodes = version.nodes
   206       val update_iterator =
   207         for {
   208           name <- domain.getOrElse(nodes.domain).iterator
   209           if !Sessions.is_hidden(name) &&
   210               !session_base.loaded_theory(name) &&
   211               !nodes.is_suppressed(name) &&
   212               !nodes(name).is_empty
   213           st = Document_Status.Node_Status.make(state, version, name)
   214           if !rep.isDefinedAt(name) || rep(name) != st
   215         } yield (name -> st)
   216       val rep1 = rep ++ update_iterator
   217       val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes.domain) else rep1
   218 
   219       if (rep == rep2) None
   220       else Some(new Nodes_Status(rep2), version.nodes.topological_order.filter(rep2.keySet))
   221     }
   222 
   223     override def hashCode: Int = rep.hashCode
   224     override def equals(that: Any): Boolean =
   225       that match {
   226         case other: Nodes_Status => rep == other.rep
   227         case _ => false
   228       }
   229 
   230     override def toString: String =
   231     {
   232       var ok = 0
   233       var failed = 0
   234       var pending = 0
   235       var canceled = 0
   236       for (name <- rep.keysIterator) {
   237         overall_node_status(name) match {
   238           case Overall_Node_Status.ok => ok += 1
   239           case Overall_Node_Status.failed => failed += 1
   240           case Overall_Node_Status.pending => pending += 1
   241         }
   242         if (apply(name).canceled) canceled += 1
   243       }
   244       "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending +
   245         ", canceled = " + canceled + ")"
   246     }
   247   }
   248 }