47 { |
47 { |
48 val init = Status() |
48 val init = Status() |
49 } |
49 } |
50 |
50 |
51 sealed case class Status( |
51 sealed case class Status( |
|
52 private val parsed: Boolean = false, |
52 private val finished: Boolean = false, |
53 private val finished: Boolean = false, |
53 private val failed: Boolean = false, |
54 private val failed: Boolean = false, |
54 forks: Int = 0) |
55 forks: Int = 0) |
55 { |
56 { |
56 def is_unprocessed: Boolean = !finished && !failed && forks == 0 |
57 def is_unprocessed: Boolean = parsed && !finished && !failed && forks == 0 |
57 def is_running: Boolean = forks != 0 |
58 def is_running: Boolean = forks != 0 |
58 def is_finished: Boolean = finished && forks == 0 |
59 def is_finished: Boolean = finished && forks == 0 |
59 def is_failed: Boolean = failed && forks == 0 |
60 def is_failed: Boolean = failed && forks == 0 |
60 def + (that: Status): Status = |
61 def + (that: Status): Status = |
61 Status(finished || that.finished, failed || that.failed, forks + that.forks) |
62 Status(parsed || that.parsed, finished || that.finished, |
|
63 failed || that.failed, forks + that.forks) |
62 } |
64 } |
63 |
65 |
64 val command_status_markup: Set[String] = |
66 val command_status_markup: Set[String] = |
65 Set(Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED, |
67 Set(Isabelle_Markup.PARSED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED, |
66 Isabelle_Markup.FORKED, Isabelle_Markup.JOINED) |
68 Isabelle_Markup.FORKED, Isabelle_Markup.JOINED) |
67 |
69 |
68 def command_status(status: Status, markup: Markup): Status = |
70 def command_status(status: Status, markup: Markup): Status = |
69 markup match { |
71 markup match { |
|
72 case Markup(Isabelle_Markup.PARSED, _) => status.copy(parsed = true) |
70 case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true) |
73 case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true) |
71 case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true) |
74 case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true) |
72 case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1) |
75 case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1) |
73 case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1) |
76 case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1) |
74 case _ => status |
77 case _ => status |