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