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