equal
deleted
inserted
replaced
273 Future.fork { |
273 Future.fork { |
274 val arg = XML.content(result.body).mkString |
274 val arg = XML.content(result.body).mkString |
275 val (tag, res) = Invoke_Scala.method(name, arg) |
275 val (tag, res) = Invoke_Scala.method(name, arg) |
276 prover.get.invoke_scala(id, tag, res) |
276 prover.get.invoke_scala(id, tag, res) |
277 } |
277 } |
|
278 case Markup.Cancel_Scala(id) => |
|
279 System.err.println("cancel_scala " + id) // FIXME cancel JVM task |
278 case _ => |
280 case _ => |
279 if (result.is_syslog) { |
281 if (result.is_syslog) { |
280 reverse_syslog ::= result.message |
282 reverse_syslog ::= result.message |
281 if (result.is_ready) { |
283 if (result.is_ready) { |
282 // FIXME move to ML side (!?) |
284 // FIXME move to ML side (!?) |