src/Pure/System/invoke_scala.scala
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 52582 31467a4b1466
child 54442 c39972ddd672
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
     1 /*  Title:      Pure/System/invoke_scala.scala
     2     Author:     Makarius
     3 
     4 JVM method invocation service via Isabelle/Scala.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.lang.reflect.{Method, Modifier, InvocationTargetException}
    11 import scala.util.matching.Regex
    12 
    13 
    14 object Invoke_Scala
    15 {
    16   /* method reflection */
    17 
    18   private val Ext = new Regex("(.*)\\.([^.]*)")
    19   private val STRING = Class.forName("java.lang.String")
    20 
    21   private def get_method(name: String): String => String =
    22     name match {
    23       case Ext(class_name, method_name) =>
    24         val m =
    25           try { Class.forName(class_name).getMethod(method_name, STRING) }
    26           catch {
    27             case _: ClassNotFoundException | _: NoSuchMethodException =>
    28               error("No such method: " + quote(name))
    29           }
    30         if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
    31         if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
    32 
    33         (arg: String) => {
    34           try { m.invoke(null, arg).asInstanceOf[String] }
    35           catch {
    36             case e: InvocationTargetException if e.getCause != null =>
    37               throw e.getCause
    38           }
    39         }
    40       case _ => error("Malformed method name: " + quote(name))
    41     }
    42 
    43 
    44   /* method invocation */
    45 
    46   object Tag extends Enumeration
    47   {
    48     val NULL = Value("0")
    49     val OK = Value("1")
    50     val ERROR = Value("2")
    51     val FAIL = Value("3")
    52     val INTERRUPT = Value("4")
    53   }
    54 
    55   def method(name: String, arg: String): (Tag.Value, String) =
    56     Exn.capture { get_method(name) } match {
    57       case Exn.Res(f) =>
    58         Exn.capture { f(arg) } match {
    59           case Exn.Res(null) => (Tag.NULL, "")
    60           case Exn.Res(res) => (Tag.OK, res)
    61           case Exn.Exn(_: InterruptedException) => (Tag.INTERRUPT, "")
    62           case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
    63         }
    64       case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
    65     }
    66 }
    67 
    68 
    69 /* protocol handler */
    70 
    71 class Invoke_Scala extends Session.Protocol_Handler
    72 {
    73   private var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
    74 
    75   private def fulfill(prover: Session.Prover,
    76     id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit = synchronized
    77   {
    78     if (futures.isDefinedAt(id)) {
    79       prover.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
    80       futures -= id
    81     }
    82   }
    83 
    84   private def cancel(prover: Session.Prover,
    85     id: String, future: java.util.concurrent.Future[Unit])
    86   {
    87     future.cancel(true)
    88     fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
    89   }
    90 
    91   private def invoke_scala(
    92     prover: Session.Prover, output: Isabelle_Process.Output): Boolean = synchronized
    93   {
    94     output.properties match {
    95       case Markup.Invoke_Scala(name, id) =>
    96         futures += (id ->
    97           default_thread_pool.submit(() =>
    98             {
    99               val arg = XML.content(output.body)
   100               val (tag, result) = Invoke_Scala.method(name, arg)
   101               fulfill(prover, id, tag, result)
   102             }))
   103         true
   104       case _ => false
   105     }
   106   }
   107 
   108   private def cancel_scala(
   109     prover: Session.Prover, output: Isabelle_Process.Output): Boolean = synchronized
   110   {
   111     output.properties match {
   112       case Markup.Cancel_Scala(id) =>
   113         futures.get(id) match {
   114           case Some(future) => cancel(prover, id, future)
   115           case None =>
   116         }
   117         true
   118       case _ => false
   119     }
   120   }
   121 
   122   override def stop(prover: Session.Prover): Unit = synchronized
   123   {
   124     for ((id, future) <- futures) cancel(prover, id, future)
   125     futures = Map.empty
   126   }
   127 
   128   val functions = Map(
   129     Markup.INVOKE_SCALA -> invoke_scala _,
   130     Markup.CANCEL_SCALA -> cancel_scala _)
   131 }
   132