|
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, |
|
18 Markup.FINISHED, Markup.FAILED) |
|
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 forks = 0 |
|
30 var runs = 0 |
|
31 for (markup <- markup_iterator) { |
|
32 markup.name match { |
|
33 case Markup.ACCEPTED => accepted = true |
|
34 case Markup.FORKED => touched = true; forks += 1 |
|
35 case Markup.JOINED => forks -= 1 |
|
36 case Markup.RUNNING => touched = true; runs += 1 |
|
37 case Markup.FINISHED => runs -= 1 |
|
38 case Markup.WARNING | Markup.LEGACY => warned = true |
|
39 case Markup.FAILED | Markup.ERROR => failed = true |
|
40 case _ => |
|
41 } |
|
42 } |
|
43 Command_Status(touched, accepted, warned, failed, forks, runs) |
|
44 } |
|
45 |
|
46 val empty = make(Iterator.empty) |
|
47 |
|
48 def merge(status_iterator: Iterator[Command_Status]): Command_Status = |
|
49 if (status_iterator.hasNext) { |
|
50 val status0 = status_iterator.next |
|
51 (status0 /: status_iterator)(_ + _) |
|
52 } |
|
53 else empty |
|
54 } |
|
55 |
|
56 sealed case class Command_Status( |
|
57 private val touched: Boolean, |
|
58 private val accepted: Boolean, |
|
59 private val warned: Boolean, |
|
60 private val failed: Boolean, |
|
61 forks: Int, |
|
62 runs: Int) |
|
63 { |
|
64 def + (that: Command_Status): Command_Status = |
|
65 Command_Status( |
|
66 touched || that.touched, |
|
67 accepted || that.accepted, |
|
68 warned || that.warned, |
|
69 failed || that.failed, |
|
70 forks + that.forks, |
|
71 runs + that.runs) |
|
72 |
|
73 def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0)) |
|
74 def is_running: Boolean = runs != 0 |
|
75 def is_warned: Boolean = warned |
|
76 def is_failed: Boolean = failed |
|
77 def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0 |
|
78 } |
|
79 |
|
80 |
|
81 /* node status */ |
|
82 |
|
83 object Node_Status |
|
84 { |
|
85 def make( |
|
86 state: Document.State, |
|
87 version: Document.Version, |
|
88 name: Document.Node.Name): Node_Status = |
|
89 { |
|
90 val node = version.nodes(name) |
|
91 |
|
92 var unprocessed = 0 |
|
93 var running = 0 |
|
94 var warned = 0 |
|
95 var failed = 0 |
|
96 var finished = 0 |
|
97 for (command <- node.commands.iterator) { |
|
98 val states = state.command_states(version, command) |
|
99 val status = Command_Status.merge(states.iterator.map(_.document_status)) |
|
100 |
|
101 if (status.is_running) running += 1 |
|
102 else if (status.is_failed) failed += 1 |
|
103 else if (status.is_warned) warned += 1 |
|
104 else if (status.is_finished) finished += 1 |
|
105 else unprocessed += 1 |
|
106 } |
|
107 val initialized = state.node_initialized(version, name) |
|
108 val consolidated = state.node_consolidated(version, name) |
|
109 |
|
110 Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated) |
|
111 } |
|
112 } |
|
113 |
|
114 sealed case class Node_Status( |
|
115 unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, |
|
116 initialized: Boolean, consolidated: Boolean) |
|
117 { |
|
118 def ok: Boolean = failed == 0 |
|
119 def total: Int = unprocessed + running + warned + failed + finished |
|
120 |
|
121 def json: JSON.Object.T = |
|
122 JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed, |
|
123 "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished, |
|
124 "initialized" -> initialized, "consolidated" -> consolidated) |
|
125 } |
|
126 |
|
127 |
|
128 /* node timing */ |
|
129 |
|
130 object Node_Timing |
|
131 { |
|
132 val empty: Node_Timing = Node_Timing(0.0, Map.empty) |
|
133 |
|
134 def make( |
|
135 state: Document.State, |
|
136 version: Document.Version, |
|
137 node: Document.Node, |
|
138 threshold: Double): Node_Timing = |
|
139 { |
|
140 var total = 0.0 |
|
141 var commands = Map.empty[Command, Double] |
|
142 for { |
|
143 command <- node.commands.iterator |
|
144 st <- state.command_states(version, command) |
|
145 } { |
|
146 val command_timing = |
|
147 (0.0 /: st.status)({ |
|
148 case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds |
|
149 case (timing, _) => timing |
|
150 }) |
|
151 total += command_timing |
|
152 if (command_timing >= threshold) commands += (command -> command_timing) |
|
153 } |
|
154 Node_Timing(total, commands) |
|
155 } |
|
156 } |
|
157 |
|
158 sealed case class Node_Timing(total: Double, commands: Map[Command, Double]) |
|
159 } |