41 } |
41 } |
42 |
42 |
43 |
43 |
44 /* toplevel transactions */ |
44 /* toplevel transactions */ |
45 |
45 |
46 sealed abstract class Status |
46 sealed case class Status( |
47 case object Unprocessed extends Status |
47 private val finished: Boolean = false, |
48 case class Forked(forks: Int) extends Status |
48 private val failed: Boolean = false, |
49 case object Finished extends Status |
49 forks: Int = 0) |
50 case object Failed extends Status |
50 { |
51 |
51 def is_unprocessed: Boolean = !finished && !failed && forks == 0 |
52 def command_status(markup: List[Markup]): Status = |
52 def is_running: Boolean = forks != 0 |
53 { |
53 def is_finished: Boolean = finished && forks == 0 |
54 val forks = (0 /: markup) { |
54 def is_failed: Boolean = failed && forks == 0 |
55 case (i, Markup(Isabelle_Markup.FORKED, _)) => i + 1 |
55 } |
56 case (i, Markup(Isabelle_Markup.JOINED, _)) => i - 1 |
56 |
57 case (i, _) => i |
57 val command_status_markup: Set[String] = |
58 } |
58 Set(Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED, |
59 if (forks != 0) Forked(forks) |
59 Isabelle_Markup.FORKED, Isabelle_Markup.JOINED) |
60 else if (markup.exists(_.name == Isabelle_Markup.FAILED)) Failed |
60 |
61 else if (markup.exists(_.name == Isabelle_Markup.FINISHED)) Finished |
61 def command_status(status: Status, markup: Markup): Status = |
62 else Unprocessed |
62 markup match { |
63 } |
63 case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true) |
|
64 case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true) |
|
65 case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1) |
|
66 case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1) |
|
67 case _ => status |
|
68 } |
|
69 |
|
70 def command_status(markups: List[Markup]): Status = |
|
71 (Status() /: markups)(command_status(_, _)) |
64 |
72 |
65 sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int) |
73 sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int) |
66 { |
74 { |
67 def total: Int = unprocessed + running + finished + failed |
75 def total: Int = unprocessed + running + finished + failed |
68 } |
76 } |
73 var unprocessed = 0 |
81 var unprocessed = 0 |
74 var running = 0 |
82 var running = 0 |
75 var finished = 0 |
83 var finished = 0 |
76 var failed = 0 |
84 var failed = 0 |
77 node.commands.foreach(command => |
85 node.commands.foreach(command => |
78 command_status(state.command_state(version, command).status) match { |
86 { |
79 case Unprocessed => unprocessed += 1 |
87 val status = command_status(state.command_state(version, command).status) |
80 case Forked(_) => running += 1 |
88 if (status.is_running) running += 1 |
81 case Finished => finished += 1 |
89 else if (status.is_finished) finished += 1 |
82 case Failed => failed += 1 |
90 else if (status.is_failed) failed += 1 |
|
91 else unprocessed += 1 |
83 }) |
92 }) |
84 Node_Status(unprocessed, running, finished, failed) |
93 Node_Status(unprocessed, running, finished, failed) |
85 } |
94 } |
86 |
95 |
87 |
96 |