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