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