88 def make( |
88 def make( |
89 markups: List[Markup] = Nil, |
89 markups: List[Markup] = Nil, |
90 warned: Boolean = false, |
90 warned: Boolean = false, |
91 failed: Boolean = false |
91 failed: Boolean = false |
92 ): Command_Status = { |
92 ): Command_Status = { |
93 var theory_status = Theory_Status.NONE |
93 var theory_status1 = Theory_Status.NONE |
94 var touched = false |
94 var touched1 = false |
95 var accepted = false |
95 var accepted1 = false |
96 var warned1 = warned |
96 var warned1 = warned |
97 var failed1 = failed |
97 var failed1 = failed |
98 var canceled = false |
98 var canceled1 = false |
99 var forks = 0 |
99 var forks1 = 0 |
100 var runs = 0 |
100 var runs1 = 0 |
101 var timings = Command_Timings.empty |
101 var timings1 = Command_Timings.empty |
102 for (markup <- markups) { |
102 for (markup <- markups) { |
103 markup.name match { |
103 markup.name match { |
104 case Markup.INITIALIZED => |
104 case Markup.INITIALIZED => |
105 theory_status = Theory_Status.merge(theory_status, Theory_Status.INITIALIZED) |
105 theory_status1 = Theory_Status.merge(theory_status1, Theory_Status.INITIALIZED) |
106 case Markup.FINALIZED => |
106 case Markup.FINALIZED => |
107 theory_status = Theory_Status.merge(theory_status, Theory_Status.FINALIZED) |
107 theory_status1 = Theory_Status.merge(theory_status1, Theory_Status.FINALIZED) |
108 case Markup.CONSOLIDATING => |
108 case Markup.CONSOLIDATING => |
109 theory_status = Theory_Status.merge(theory_status, Theory_Status.CONSOLIDATING) |
109 theory_status1 = Theory_Status.merge(theory_status1, Theory_Status.CONSOLIDATING) |
110 case Markup.CONSOLIDATED => |
110 case Markup.CONSOLIDATED => |
111 theory_status = Theory_Status.merge(theory_status, Theory_Status.CONSOLIDATED) |
111 theory_status1 = Theory_Status.merge(theory_status1, Theory_Status.CONSOLIDATED) |
112 case Markup.ACCEPTED => accepted = true |
112 case Markup.ACCEPTED => accepted1 = true |
113 case Markup.FORKED => touched = true; forks += 1 |
113 case Markup.FORKED => touched1 = true; forks1 += 1 |
114 case Markup.JOINED => forks -= 1 |
114 case Markup.JOINED => forks1 -= 1 |
115 case Markup.RUNNING => touched = true; runs += 1 |
115 case Markup.RUNNING => touched1 = true; runs1 += 1 |
116 case Markup.FINISHED => runs -= 1 |
116 case Markup.FINISHED => runs1 -= 1 |
117 case Markup.WARNING | Markup.LEGACY => warned1 = true |
117 case Markup.WARNING | Markup.LEGACY => warned1 = true |
118 case Markup.FAILED | Markup.ERROR => failed1 = true |
118 case Markup.FAILED | Markup.ERROR => failed1 = true |
119 case Markup.CANCELED => canceled = true |
119 case Markup.CANCELED => canceled1 = true |
120 case Markup.TIMING => |
120 case Markup.TIMING => |
121 val props = markup.properties |
121 val props = markup.properties |
122 val offset = Position.Offset.get(props) |
122 val offset = Position.Offset.get(props) |
123 val timing = Markup.Timing_Properties.get(props) |
123 val timing = Markup.Timing_Properties.get(props) |
124 timings += (offset -> timing) |
124 timings1 += (offset -> timing) |
125 case _ => |
125 case _ => |
126 } |
126 } |
127 } |
127 } |
128 new Command_Status( |
128 new Command_Status( |
129 theory_status = theory_status, |
129 theory_status = theory_status1, |
130 touched = touched, |
130 touched = touched1, |
131 accepted = accepted, |
131 accepted = accepted1, |
132 warned = warned1, |
132 warned = warned1, |
133 failed = failed1, |
133 failed = failed1, |
134 canceled = canceled, |
134 canceled = canceled1, |
135 forks = forks, |
135 forks = forks1, |
136 runs = runs, |
136 runs = runs1, |
137 timings = timings) |
137 timings = timings1) |
138 } |
138 } |
139 |
139 |
140 val empty: Command_Status = make() |
140 val empty: Command_Status = make() |
141 |
141 |
142 def merge(args: IterableOnce[Command_Status]): Command_Status = |
142 def merge(args: IterableOnce[Command_Status]): Command_Status = |