102 case object Event |
102 case object Event |
103 |
103 |
104 |
104 |
105 /* manager actor */ |
105 /* manager actor */ |
106 |
106 |
107 private case class Handle_Results(session: Session, id: Document_ID.Command, results: Command.Results) |
107 private case class Handle_Results( |
|
108 session: Session, id: Document_ID.Command, results: Command.Results) |
108 private case class Generate_Trace(results: Command.Results) |
109 private case class Generate_Trace(results: Command.Results) |
109 private case class Cancel(serial: Long) |
110 private case class Cancel(serial: Long) |
110 private object Clear_Memory |
111 private object Clear_Memory |
111 private object Stop |
112 private object Stop |
112 case class Reply(session: Session, serial: Long, answer: Answer) |
113 case class Reply(session: Session, serial: Long, answer: Answer) |
113 |
114 |
114 case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer) |
115 case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer) |
115 |
116 |
116 case class Context( |
117 case class Context( |
117 last_serial: Long = 0L, |
118 last_serial: Long = 0L, |
118 questions: SortedMap[Long, Question] = SortedMap.empty |
119 questions: SortedMap[Long, Question] = SortedMap.empty) |
119 ) |
120 { |
120 { |
|
121 |
|
122 def +(q: Question): Context = |
121 def +(q: Question): Context = |
123 copy(questions = questions + ((q.data.serial, q))) |
122 copy(questions = questions + ((q.data.serial, q))) |
124 |
123 |
125 def -(s: Long): Context = |
124 def -(s: Long): Context = |
126 copy(questions = questions - s) |
125 copy(questions = questions - s) |
127 |
126 |
128 def with_serial(s: Long): Context = |
127 def with_serial(s: Long): Context = |
129 copy(last_serial = Math.max(last_serial, s)) |
128 copy(last_serial = Math.max(last_serial, s)) |
130 |
|
131 } |
129 } |
132 |
130 |
133 case class Trace(entries: List[Item.Data]) |
131 case class Trace(entries: List[Item.Data]) |
134 |
132 |
135 case class Index(text: String, content: XML.Body) |
133 case class Index(text: String, content: XML.Body) |
173 contexts += (id -> (contexts(id) - serial)) |
171 contexts += (id -> (contexts(id) - serial)) |
174 } |
172 } |
175 |
173 |
176 def do_reply(session: Session, serial: Long, answer: Answer) |
174 def do_reply(session: Session, serial: Long, answer: Answer) |
177 { |
175 { |
178 session.protocol_command("Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name) |
176 session.protocol_command( |
|
177 "Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name) |
179 } |
178 } |
180 |
179 |
181 loop { |
180 loop { |
182 react { |
181 react { |
183 case Handle_Results(session, id, results) => |
182 case Handle_Results(session, id, results) => |
186 |
185 |
187 for ((serial, result) <- results.iterator if serial > new_context.last_serial) |
186 for ((serial, result) <- results.iterator if serial > new_context.last_serial) |
188 { |
187 { |
189 result match { |
188 result match { |
190 case Item(markup, data) => |
189 case Item(markup, data) => |
191 memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial)) |
190 memory_children += |
|
191 (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial)) |
192 |
192 |
193 markup match { |
193 markup match { |
194 |
194 |
195 case Markup.SIMP_TRACE_STEP => |
195 case Markup.SIMP_TRACE_STEP => |
196 val index = Index.of_data(data) |
196 val index = Index.of_data(data) |
204 case Markup.SIMP_TRACE_HINT => |
204 case Markup.SIMP_TRACE_HINT => |
205 data.props match { |
205 data.props match { |
206 case Success(false) => |
206 case Success(false) => |
207 results.get(data.parent) match { |
207 results.get(data.parent) match { |
208 case Some(Item(Markup.SIMP_TRACE_STEP, _)) => |
208 case Some(Item(Markup.SIMP_TRACE_STEP, _)) => |
209 new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default) |
209 new_context += |
|
210 Question(data, Answer.hint_fail.all, Answer.hint_fail.default) |
210 case _ => |
211 case _ => |
211 // unknown, better send a default reply |
212 // unknown, better send a default reply |
212 do_reply(session, data.serial, Answer.hint_fail.default) |
213 do_reply(session, data.serial, Answer.hint_fail.default) |
213 } |
214 } |
214 case _ => |
215 case _ => |