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