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