src/Pure/System/invoke_scala.scala
changeset 52111 1fd184eaa310
parent 49470 ee564db2649b
child 52582 31467a4b1466
     1.1 --- a/src/Pure/System/invoke_scala.scala	Wed May 22 08:46:39 2013 +0200
     1.2 +++ b/src/Pure/System/invoke_scala.scala	Wed May 22 14:10:45 2013 +0200
     1.3 @@ -64,3 +64,69 @@
     1.4        case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
     1.5      }
     1.6  }
     1.7 +
     1.8 +
     1.9 +/* protocol handler */
    1.10 +
    1.11 +class Invoke_Scala extends Session.Protocol_Handler
    1.12 +{
    1.13 +  private var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
    1.14 +
    1.15 +  private def fulfill(prover: Session.Prover,
    1.16 +    id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit = synchronized
    1.17 +  {
    1.18 +    if (futures.isDefinedAt(id)) {
    1.19 +      prover.input("Invoke_Scala.fulfill", id, tag.toString, res)
    1.20 +      futures -= id
    1.21 +    }
    1.22 +  }
    1.23 +
    1.24 +  private def cancel(prover: Session.Prover,
    1.25 +    id: String, future: java.util.concurrent.Future[Unit])
    1.26 +  {
    1.27 +    future.cancel(true)
    1.28 +    fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
    1.29 +  }
    1.30 +
    1.31 +  private def invoke_scala(
    1.32 +    prover: Session.Prover, output: Isabelle_Process.Output): Boolean = synchronized
    1.33 +  {
    1.34 +    output.properties match {
    1.35 +      case Markup.Invoke_Scala(name, id) =>
    1.36 +        futures += (id ->
    1.37 +          default_thread_pool.submit(() =>
    1.38 +            {
    1.39 +              val arg = XML.content(output.body)
    1.40 +              val (tag, result) = Invoke_Scala.method(name, arg)
    1.41 +              fulfill(prover, id, tag, result)
    1.42 +            }))
    1.43 +        true
    1.44 +      case _ => false
    1.45 +    }
    1.46 +  }
    1.47 +
    1.48 +  private def cancel_scala(
    1.49 +    prover: Session.Prover, output: Isabelle_Process.Output): Boolean = synchronized
    1.50 +  {
    1.51 +    output.properties match {
    1.52 +      case Markup.Cancel_Scala(id) =>
    1.53 +        futures.get(id) match {
    1.54 +          case Some(future) => cancel(prover, id, future)
    1.55 +          case None =>
    1.56 +        }
    1.57 +        true
    1.58 +      case _ => false
    1.59 +    }
    1.60 +  }
    1.61 +
    1.62 +  override def stop(prover: Session.Prover): Unit = synchronized
    1.63 +  {
    1.64 +    for ((id, future) <- futures) cancel(prover, id, future)
    1.65 +    futures = Map.empty
    1.66 +  }
    1.67 +
    1.68 +  val functions = Map(
    1.69 +    Markup.INVOKE_SCALA -> invoke_scala _,
    1.70 +    Markup.CANCEL_SCALA -> cancel_scala _)
    1.71 +}
    1.72 +