1/*  Title:      Pure/PIDE/document_status.scala
2    Author:     Makarius
3
4Document status based on markup information.
5*/
6
7package isabelle
8
9
10object 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}
307