src/Pure/PIDE/document_status.scala

clarified quasi_consolidated status after 5f160df596c1 -- relevant for headless PIDE session (e.g. "isabelle dump");

/*  Title:      Pure/PIDE/document_status.scala
    Author:     Makarius

Document status based on markup information.
*/

package isabelle


object Document_Status
{
  /* command status */

  object Command_Status
  {
    val proper_elements: Markup.Elements =
      Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
        Markup.FINISHED, Markup.FAILED, Markup.CANCELED)

    val liberal_elements: Markup.Elements =
      proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR

    def make(markup_iterator: Iterator[Markup]): Command_Status =
    {
      var touched = false
      var accepted = false
      var warned = false
      var failed = false
      var canceled = false
      var finalized = false
      var forks = 0
      var runs = 0
      for (markup <- markup_iterator) {
        markup.name match {
          case Markup.ACCEPTED => accepted = true
          case Markup.FORKED => touched = true; forks += 1
          case Markup.JOINED => forks -= 1
          case Markup.RUNNING => touched = true; runs += 1
          case Markup.FINISHED => runs -= 1
          case Markup.WARNING | Markup.LEGACY => warned = true
          case Markup.FAILED | Markup.ERROR => failed = true
          case Markup.CANCELED => canceled = true
          case Markup.FINALIZED => finalized = true
          case _ =>
        }
      }
      Command_Status(
        touched = touched,
        accepted = accepted,
        warned = warned,
        failed = failed,
        canceled = canceled,
        finalized = finalized,
        forks = forks,
        runs = runs)
    }

    val empty = make(Iterator.empty)

    def merge(status_iterator: Iterator[Command_Status]): Command_Status =
      if (status_iterator.hasNext) {
        val status0 = status_iterator.next
        (status0 /: status_iterator)(_ + _)
      }
      else empty
  }

  sealed case class Command_Status(
    private val touched: Boolean,
    private val accepted: Boolean,
    private val warned: Boolean,
    private val failed: Boolean,
    private val canceled: Boolean,
    private val finalized: Boolean,
    forks: Int,
    runs: Int)
  {
    def + (that: Command_Status): Command_Status =
      Command_Status(
        touched = touched || that.touched,
        accepted = accepted || that.accepted,
        warned = warned || that.warned,
        failed = failed || that.failed,
        canceled = canceled || that.canceled,
        finalized = finalized || that.finalized,
        forks = forks + that.forks,
        runs = runs + that.runs)

    def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
    def is_running: Boolean = runs != 0
    def is_warned: Boolean = warned
    def is_failed: Boolean = failed
    def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    def is_canceled: Boolean = canceled
    def is_finalized: Boolean = finalized
    def is_terminated: Boolean = canceled || touched && forks == 0 && runs == 0
  }


  /* node status */

  object Node_Status
  {
    def make(
      state: Document.State,
      version: Document.Version,
      name: Document.Node.Name): Node_Status =
    {
      val node = version.nodes(name)

      var unprocessed = 0
      var running = 0
      var warned = 0
      var failed = 0
      var finished = 0
      var canceled = false
      var terminated = true
      var finalized = false
      for (command <- node.commands.iterator) {
        val states = state.command_states(version, command)
        val status = Command_Status.merge(states.iterator.map(_.document_status))

        if (status.is_running) running += 1
        else if (status.is_failed) failed += 1
        else if (status.is_warned) warned += 1
        else if (status.is_finished) finished += 1
        else unprocessed += 1

        if (status.is_canceled) canceled = true
        if (!status.is_terminated) terminated = false
        if (status.is_finalized) finalized = true
      }
      val initialized = state.node_initialized(version, name)
      val consolidated = state.node_consolidated(version, name)

      Node_Status(
        is_suppressed = version.nodes.is_suppressed(name),
        unprocessed = unprocessed,
        running = running,
        warned = warned,
        failed = failed,
        finished = finished,
        canceled = canceled,
        terminated = terminated,
        initialized = initialized,
        finalized = finalized,
        consolidated = consolidated)
    }
  }

  sealed case class Node_Status(
    is_suppressed: Boolean,
    unprocessed: Int,
    running: Int,
    warned: Int,
    failed: Int,
    finished: Int,
    canceled: Boolean,
    terminated: Boolean,
    initialized: Boolean,
    finalized: Boolean,
    consolidated: Boolean)
  {
    def ok: Boolean = failed == 0
    def total: Int = unprocessed + running + warned + failed + finished

    def quasi_consolidated: Boolean = !is_suppressed && !finalized && terminated

    def percentage: Int =
      if (consolidated) 100
      else if (total == 0) 0
      else (((total - unprocessed).toDouble / total) * 100).toInt min 99

    def json: JSON.Object.T =
      JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
        "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
        "canceled" -> canceled, "consolidated" -> consolidated,
        "percentage" -> percentage)
  }


  /* node timing */

  object Node_Timing
  {
    val empty: Node_Timing = Node_Timing(0.0, Map.empty)

    def make(
      state: Document.State,
      version: Document.Version,
      node: Document.Node,
      threshold: Double): Node_Timing =
    {
      var total = 0.0
      var commands = Map.empty[Command, Double]
      for {
        command <- node.commands.iterator
        st <- state.command_states(version, command)
      } {
        val command_timing =
          (0.0 /: st.status)({
            case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
            case (timing, _) => timing
          })
        total += command_timing
        if (command_timing >= threshold) commands += (command -> command_timing)
      }
      Node_Timing(total, commands)
    }
  }

  sealed case class Node_Timing(total: Double, commands: Map[Command, Double])


  /* nodes status */

  object Overall_Node_Status extends Enumeration
  {
    val ok, failed, pending = Value
  }

  object Nodes_Status
  {
    val empty: Nodes_Status = new Nodes_Status(Map.empty, Document.Nodes.empty)
  }

  final class Nodes_Status private(
    private val rep: Map[Document.Node.Name, Node_Status],
    nodes: Document.Nodes)
  {
    def is_empty: Boolean = rep.isEmpty
    def apply(name: Document.Node.Name): Node_Status = rep(name)
    def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)

    def present: List[(Document.Node.Name, Node_Status)] =
      (for {
        name <- nodes.topological_order.iterator
        node_status <- get(name)
      } yield (name, node_status)).toList

    def quasi_consolidated(name: Document.Node.Name): Boolean =
      rep.get(name) match {
        case Some(st) => st.quasi_consolidated
        case None => false
      }

    def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
      rep.get(name) match {
        case Some(st) if st.consolidated =>
          if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
        case _ => Overall_Node_Status.pending
      }

    def update(
      resources: Resources,
      state: Document.State,
      version: Document.Version,
      domain: Option[Set[Document.Node.Name]] = None,
      trim: Boolean = false): (Boolean, Nodes_Status) =
    {
      val nodes1 = version.nodes
      val update_iterator =
        for {
          name <- domain.getOrElse(nodes1.domain).iterator
          if !resources.is_hidden(name) && !resources.session_base.loaded_theory(name)
          st = Document_Status.Node_Status.make(state, version, name)
          if !rep.isDefinedAt(name) || rep(name) != st
        } yield (name -> st)
      val rep1 = rep ++ update_iterator
      val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes1.domain) else rep1

      (rep != rep2, new Nodes_Status(rep2, nodes1))
    }

    override def hashCode: Int = rep.hashCode
    override def equals(that: Any): Boolean =
      that match {
        case other: Nodes_Status => rep == other.rep
        case _ => false
      }

    override def toString: String =
    {
      var ok = 0
      var failed = 0
      var pending = 0
      var canceled = 0
      for (name <- rep.keysIterator) {
        overall_node_status(name) match {
          case Overall_Node_Status.ok => ok += 1
          case Overall_Node_Status.failed => failed += 1
          case Overall_Node_Status.pending => pending += 1
        }
        if (apply(name).canceled) canceled += 1
      }
      "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending +
        ", canceled = " + canceled + ")"
    }
  }
}