136 { |
136 { |
137 for ((id, future) <- futures) cancel(id, future) |
137 for ((id, future) <- futures) cancel(id, future) |
138 futures = Map.empty |
138 futures = Map.empty |
139 } |
139 } |
140 |
140 |
141 private def fulfill(id: String, tag: Scala.Tag.Value, res: String): Unit = |
141 private def result(id: String, tag: Scala.Tag.Value, res: String): Unit = |
142 synchronized |
142 synchronized |
143 { |
143 { |
144 if (futures.isDefinedAt(id)) { |
144 if (futures.isDefinedAt(id)) { |
145 session.protocol_command("Scala.fulfill", id, tag.id.toString, res) |
145 session.protocol_command("Scala.result", id, tag.id.toString, res) |
146 futures -= id |
146 futures -= id |
147 } |
147 } |
148 } |
148 } |
149 |
149 |
150 private def cancel(id: String, future: Future[Unit]) |
150 private def cancel(id: String, future: Future[Unit]) |
151 { |
151 { |
152 future.cancel |
152 future.cancel |
153 fulfill(id, Scala.Tag.INTERRUPT, "") |
153 result(id, Scala.Tag.INTERRUPT, "") |
154 } |
154 } |
155 |
155 |
156 private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized |
156 private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized |
157 { |
157 { |
158 msg.properties match { |
158 msg.properties match { |
159 case Markup.Invoke_Scala(name, id) => |
159 case Markup.Invoke_Scala(name, id) => |
160 futures += (id -> |
160 futures += (id -> |
161 Future.fork { |
161 Future.fork { |
162 val (tag, result) = Scala.function(name, msg.text) |
162 val (tag, res) = Scala.function(name, msg.text) |
163 fulfill(id, tag, result) |
163 result(id, tag, res) |
164 }) |
164 }) |
165 true |
165 true |
166 case _ => false |
166 case _ => false |
167 } |
167 } |
168 } |
168 } |