src/Pure/PIDE/document_status.scala
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 70045 d594997cdcf4
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
     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         is_suppressed = version.nodes.is_suppressed(name),
   138         unprocessed = unprocessed,
   139         running = running,
   140         warned = warned,
   141         failed = failed,
   142         finished = finished,
   143         canceled = canceled,
   144         terminated = terminated,
   145         initialized = initialized,
   146         finalized = finalized,
   147         consolidated = consolidated)
   148     }
   149   }
   150 
   151   sealed case class Node_Status(
   152     is_suppressed: Boolean,
   153     unprocessed: Int,
   154     running: Int,
   155     warned: Int,
   156     failed: Int,
   157     finished: Int,
   158     canceled: Boolean,
   159     terminated: Boolean,
   160     initialized: Boolean,
   161     finalized: Boolean,
   162     consolidated: Boolean)
   163   {
   164     def ok: Boolean = failed == 0
   165     def total: Int = unprocessed + running + warned + failed + finished
   166 
   167     def quasi_consolidated: Boolean = !is_suppressed && !finalized && terminated
   168 
   169     def percentage: Int =
   170       if (consolidated) 100
   171       else if (total == 0) 0
   172       else (((total - unprocessed).toDouble / total) * 100).toInt min 99
   173 
   174     def json: JSON.Object.T =
   175       JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
   176         "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
   177         "canceled" -> canceled, "consolidated" -> consolidated,
   178         "percentage" -> percentage)
   179   }
   180 
   181 
   182   /* overall timing */
   183 
   184   object Overall_Timing
   185   {
   186     val empty: Overall_Timing = Overall_Timing(0.0, Map.empty)
   187 
   188     def make(
   189       state: Document.State,
   190       version: Document.Version,
   191       commands: Iterable[Command],
   192       threshold: Double = 0.0): Overall_Timing =
   193     {
   194       var total = 0.0
   195       var command_timings = Map.empty[Command, Double]
   196       for {
   197         command <- commands.iterator
   198         st <- state.command_states(version, command)
   199       } {
   200         val command_timing =
   201           (0.0 /: st.status)({
   202             case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
   203             case (timing, _) => timing
   204           })
   205         total += command_timing
   206         if (command_timing > 0.0 && command_timing >= threshold) {
   207           command_timings += (command -> command_timing)
   208         }
   209       }
   210       Overall_Timing(total, command_timings)
   211     }
   212   }
   213 
   214   sealed case class Overall_Timing(total: Double, command_timings: Map[Command, Double])
   215   {
   216     def command_timing(command: Command): Double =
   217       command_timings.getOrElse(command, 0.0)
   218   }
   219 
   220 
   221   /* nodes status */
   222 
   223   object Overall_Node_Status extends Enumeration
   224   {
   225     val ok, failed, pending = Value
   226   }
   227 
   228   object Nodes_Status
   229   {
   230     val empty: Nodes_Status = new Nodes_Status(Map.empty, Document.Nodes.empty)
   231   }
   232 
   233   final class Nodes_Status private(
   234     private val rep: Map[Document.Node.Name, Node_Status],
   235     nodes: Document.Nodes)
   236   {
   237     def is_empty: Boolean = rep.isEmpty
   238     def apply(name: Document.Node.Name): Node_Status = rep(name)
   239     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
   240 
   241     def present: List[(Document.Node.Name, Node_Status)] =
   242       (for {
   243         name <- nodes.topological_order.iterator
   244         node_status <- get(name)
   245       } yield (name, node_status)).toList
   246 
   247     def quasi_consolidated(name: Document.Node.Name): Boolean =
   248       rep.get(name) match {
   249         case Some(st) => st.quasi_consolidated
   250         case None => false
   251       }
   252 
   253     def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
   254       rep.get(name) match {
   255         case Some(st) if st.consolidated =>
   256           if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
   257         case _ => Overall_Node_Status.pending
   258       }
   259 
   260     def update(
   261       resources: Resources,
   262       state: Document.State,
   263       version: Document.Version,
   264       domain: Option[Set[Document.Node.Name]] = None,
   265       trim: Boolean = false): (Boolean, Nodes_Status) =
   266     {
   267       val nodes1 = version.nodes
   268       val update_iterator =
   269         for {
   270           name <- domain.getOrElse(nodes1.domain).iterator
   271           if !resources.is_hidden(name) && !resources.session_base.loaded_theory(name)
   272           st = Document_Status.Node_Status.make(state, version, name)
   273           if !rep.isDefinedAt(name) || rep(name) != st
   274         } yield (name -> st)
   275       val rep1 = rep ++ update_iterator
   276       val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes1.domain) else rep1
   277 
   278       (rep != rep2, new Nodes_Status(rep2, nodes1))
   279     }
   280 
   281     override def hashCode: Int = rep.hashCode
   282     override def equals(that: Any): Boolean =
   283       that match {
   284         case other: Nodes_Status => rep == other.rep
   285         case _ => false
   286       }
   287 
   288     override def toString: String =
   289     {
   290       var ok = 0
   291       var failed = 0
   292       var pending = 0
   293       var canceled = 0
   294       for (name <- rep.keysIterator) {
   295         overall_node_status(name) match {
   296           case Overall_Node_Status.ok => ok += 1
   297           case Overall_Node_Status.failed => failed += 1
   298           case Overall_Node_Status.pending => pending += 1
   299         }
   300         if (apply(name).canceled) canceled += 1
   301       }
   302       "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending +
   303         ", canceled = " + canceled + ")"
   304     }
   305   }
   306 }