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