src/Pure/PIDE/document_status.scala
author wenzelm
Sun Sep 02 21:22:52 2018 +0200 (15 months ago ago)
changeset 68883 3653b3ad729e
parent 68881 d975449b266e
child 68884 9b97d0b20d95
permissions -rw-r--r--
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
     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     def is_terminated: Boolean = canceled || touched && forks == 0 && runs == 0
    84   }
    85 
    86 
    87   /* node status */
    88 
    89   object Node_Status
    90   {
    91     def make(
    92       state: Document.State,
    93       version: Document.Version,
    94       name: Document.Node.Name): Node_Status =
    95     {
    96       val node = version.nodes(name)
    97 
    98       var unprocessed = 0
    99       var running = 0
   100       var warned = 0
   101       var failed = 0
   102       var finished = 0
   103       var canceled = false
   104       var terminated = false
   105       for (command <- node.commands.iterator) {
   106         val states = state.command_states(version, command)
   107         val status = Command_Status.merge(states.iterator.map(_.document_status))
   108 
   109         if (status.is_running) running += 1
   110         else if (status.is_failed) failed += 1
   111         else if (status.is_warned) warned += 1
   112         else if (status.is_finished) finished += 1
   113         else unprocessed += 1
   114 
   115         if (status.is_canceled) canceled = true
   116         if (status.is_terminated) terminated = true
   117       }
   118       val initialized = state.node_initialized(version, name)
   119       val consolidated = state.node_consolidated(version, name)
   120 
   121       Node_Status(unprocessed, running, warned, failed, finished, canceled, terminated,
   122         initialized, consolidated)
   123     }
   124   }
   125 
   126   sealed case class Node_Status(
   127     unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
   128     canceled: Boolean, terminated: Boolean, initialized: Boolean, consolidated: Boolean)
   129   {
   130     def ok: Boolean = failed == 0
   131     def total: Int = unprocessed + running + warned + failed + finished
   132 
   133     def json: JSON.Object.T =
   134       JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
   135         "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
   136         "canceled" -> canceled, "terminated" -> terminated, "initialized" -> initialized,
   137         "consolidated" -> consolidated)
   138   }
   139 
   140 
   141   /* node timing */
   142 
   143   object Node_Timing
   144   {
   145     val empty: Node_Timing = Node_Timing(0.0, Map.empty)
   146 
   147     def make(
   148       state: Document.State,
   149       version: Document.Version,
   150       node: Document.Node,
   151       threshold: Double): Node_Timing =
   152     {
   153       var total = 0.0
   154       var commands = Map.empty[Command, Double]
   155       for {
   156         command <- node.commands.iterator
   157         st <- state.command_states(version, command)
   158       } {
   159         val command_timing =
   160           (0.0 /: st.status)({
   161             case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
   162             case (timing, _) => timing
   163           })
   164         total += command_timing
   165         if (command_timing >= threshold) commands += (command -> command_timing)
   166       }
   167       Node_Timing(total, commands)
   168     }
   169   }
   170 
   171   sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
   172 
   173 
   174   /* nodes status */
   175 
   176   object Overall_Node_Status extends Enumeration
   177   {
   178     val ok, failed, pending = Value
   179   }
   180 
   181   object Nodes_Status
   182   {
   183     val empty: Nodes_Status = new Nodes_Status(Map.empty)
   184 
   185     type Update = (Nodes_Status, List[Document.Node.Name])
   186     val empty_update: Update = (empty, Nil)
   187   }
   188 
   189   final class Nodes_Status private(private val rep: Map[Document.Node.Name, Node_Status])
   190   {
   191     def is_empty: Boolean = rep.isEmpty
   192     def apply(name: Document.Node.Name): Node_Status = rep(name)
   193     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
   194 
   195     def is_terminated(name: Document.Node.Name): Boolean =
   196       rep.get(name) match {
   197         case Some(st) => st.terminated
   198         case None => false
   199       }
   200 
   201     def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
   202       rep.get(name) match {
   203         case Some(st) if st.consolidated =>
   204           if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
   205         case _ => Overall_Node_Status.pending
   206       }
   207 
   208     def update(
   209       session_base: Sessions.Base,
   210       state: Document.State,
   211       version: Document.Version,
   212       domain: Option[Set[Document.Node.Name]] = None,
   213       trim: Boolean = false): Option[Nodes_Status.Update] =
   214     {
   215       val nodes = version.nodes
   216       val update_iterator =
   217         for {
   218           name <- domain.getOrElse(nodes.domain).iterator
   219           if !Sessions.is_hidden(name) &&
   220               !session_base.loaded_theory(name) &&
   221               !nodes.is_suppressed(name) &&
   222               !nodes(name).is_empty
   223           st = Document_Status.Node_Status.make(state, version, name)
   224           if !rep.isDefinedAt(name) || rep(name) != st
   225         } yield (name -> st)
   226       val rep1 = rep ++ update_iterator
   227       val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes.domain) else rep1
   228 
   229       if (rep == rep2) None
   230       else Some(new Nodes_Status(rep2), version.nodes.topological_order.filter(rep2.keySet))
   231     }
   232 
   233     override def hashCode: Int = rep.hashCode
   234     override def equals(that: Any): Boolean =
   235       that match {
   236         case other: Nodes_Status => rep == other.rep
   237         case _ => false
   238       }
   239 
   240     override def toString: String =
   241     {
   242       var ok = 0
   243       var failed = 0
   244       var pending = 0
   245       var canceled = 0
   246       for (name <- rep.keysIterator) {
   247         overall_node_status(name) match {
   248           case Overall_Node_Status.ok => ok += 1
   249           case Overall_Node_Status.failed => failed += 1
   250           case Overall_Node_Status.pending => pending += 1
   251         }
   252         if (apply(name).canceled) canceled += 1
   253       }
   254       "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending +
   255         ", canceled = " + canceled + ")"
   256     }
   257   }
   258 }