JVM method invocation service via Scala layer;
authorwenzelm
Mon Jul 11 16:48:02 2011 +0200 (2011-07-11)
changeset 43748c70bd78ec83c
parent 43747 74a9e9c8d5e8
child 43749 5ca34f21cb44
JVM method invocation service via Scala layer;
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Pure/General/output.ML
src/Pure/IsaMakefile
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/ROOT.ML
src/Pure/System/invoke_scala.ML
src/Pure/System/invoke_scala.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/General/markup.ML	Mon Jul 11 15:56:30 2011 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Mon Jul 11 16:48:02 2011 +0200
     1.3 @@ -117,6 +117,8 @@
     1.4    val reportN: string val report: T
     1.5    val no_reportN: string val no_report: T
     1.6    val badN: string val bad: T
     1.7 +  val functionN: string
     1.8 +  val invoke_scala: string -> string -> Properties.T
     1.9    val no_output: Output.output * Output.output
    1.10    val default_output: T -> Output.output * Output.output
    1.11    val add_mode: string -> (T -> Output.output * Output.output) -> unit
    1.12 @@ -368,6 +370,13 @@
    1.13  val (badN, bad) = markup_elem "bad";
    1.14  
    1.15  
    1.16 +(* raw message functions *)
    1.17 +
    1.18 +val functionN = "function"
    1.19 +
    1.20 +fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
    1.21 +
    1.22 +
    1.23  
    1.24  (** print mode operations **)
    1.25  
     2.1 --- a/src/Pure/General/markup.scala	Mon Jul 11 15:56:30 2011 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Mon Jul 11 16:48:02 2011 +0200
     2.3 @@ -333,6 +333,22 @@
     2.4    val READY = "ready"
     2.5  
     2.6  
     2.7 +  /* raw message functions */
     2.8 +
     2.9 +  val FUNCTION = "function"
    2.10 +  val Function = new Property(FUNCTION)
    2.11 +
    2.12 +  val INVOKE_SCALA = "invoke_scala"
    2.13 +  object Invoke_Scala
    2.14 +  {
    2.15 +    def unapply(props: List[(String, String)]): Option[(String, String)] =
    2.16 +      props match {
    2.17 +        case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
    2.18 +        case _ => None
    2.19 +      }
    2.20 +  }
    2.21 +
    2.22 +
    2.23    /* system data */
    2.24  
    2.25    val Data = Markup("data", Nil)
     3.1 --- a/src/Pure/General/output.ML	Mon Jul 11 15:56:30 2011 +0200
     3.2 +++ b/src/Pure/General/output.ML	Mon Jul 11 16:48:02 2011 +0200
     3.3 @@ -96,7 +96,9 @@
     3.4    val prompt_fn = Unsynchronized.ref raw_stdout;
     3.5    val status_fn = Unsynchronized.ref (fn _: output => ());
     3.6    val report_fn = Unsynchronized.ref (fn _: output => ());
     3.7 -  val raw_message_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
     3.8 +  val raw_message_fn =
     3.9 +    Unsynchronized.ref
    3.10 +      (fn _: Properties.T => fn _: output => raise Fail "Output.raw_message undefined");
    3.11  end;
    3.12  
    3.13  fun writeln s = ! Private_Hooks.writeln_fn (output s);
     4.1 --- a/src/Pure/IsaMakefile	Mon Jul 11 15:56:30 2011 +0200
     4.2 +++ b/src/Pure/IsaMakefile	Mon Jul 11 16:48:02 2011 +0200
     4.3 @@ -189,6 +189,7 @@
     4.4    Syntax/syntax_phases.ML				\
     4.5    Syntax/syntax_trans.ML				\
     4.6    Syntax/term_position.ML				\
     4.7 +  System/invoke_scala.ML				\
     4.8    System/isabelle_process.ML				\
     4.9    System/isabelle_system.ML				\
    4.10    System/isar.ML					\
     5.1 --- a/src/Pure/PIDE/isar_document.ML	Mon Jul 11 15:56:30 2011 +0200
     5.2 +++ b/src/Pure/PIDE/isar_document.ML	Mon Jul 11 16:48:02 2011 +0200
     5.3 @@ -33,5 +33,9 @@
     5.4        val state'' = Document.execute new_id state';
     5.5      in state'' end));
     5.6  
     5.7 +val _ =
     5.8 +  Isabelle_Process.add_command "Isar_Document.invoke_scala"
     5.9 +    (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
    5.10 +
    5.11  end;
    5.12  
     6.1 --- a/src/Pure/PIDE/isar_document.scala	Mon Jul 11 15:56:30 2011 +0200
     6.2 +++ b/src/Pure/PIDE/isar_document.scala	Mon Jul 11 16:48:02 2011 +0200
     6.3 @@ -154,4 +154,12 @@
     6.4        Document.ID(old_id), Document.ID(new_id),
     6.5          YXML.string_of_body(arg1), YXML.string_of_body(arg2))
     6.6    }
     6.7 +
     6.8 +
     6.9 +  /* method invocation service */
    6.10 +
    6.11 +  def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
    6.12 +  {
    6.13 +    input("Isar_Document.invoke_scala", id, tag.toString, res)
    6.14 +  }
    6.15  }
     7.1 --- a/src/Pure/ROOT.ML	Mon Jul 11 15:56:30 2011 +0200
     7.2 +++ b/src/Pure/ROOT.ML	Mon Jul 11 16:48:02 2011 +0200
     7.3 @@ -274,6 +274,7 @@
     7.4  
     7.5  use "System/session.ML";
     7.6  use "System/isabelle_process.ML";
     7.7 +use "System/invoke_scala.ML";
     7.8  use "PIDE/isar_document.ML";
     7.9  use "System/isar.ML";
    7.10  
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/System/invoke_scala.ML	Mon Jul 11 16:48:02 2011 +0200
     8.3 @@ -0,0 +1,58 @@
     8.4 +(*  Title:      Pure/System/invoke_scala.ML
     8.5 +    Author:     Makarius
     8.6 +
     8.7 +JVM method invocation service via Scala layer.
     8.8 +
     8.9 +TODO: proper cancellation!
    8.10 +*)
    8.11 +
    8.12 +signature INVOKE_SCALA =
    8.13 +sig
    8.14 +  val method: string -> string -> string future
    8.15 +  exception Null
    8.16 +  val fulfill_method: string -> string -> string -> unit
    8.17 +end;
    8.18 +
    8.19 +structure Invoke_Scala: INVOKE_SCALA =
    8.20 +struct
    8.21 +
    8.22 +(* pending promises *)
    8.23 +
    8.24 +val new_id = string_of_int o Synchronized.counter ();
    8.25 +
    8.26 +val promises =
    8.27 +  Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
    8.28 +
    8.29 +
    8.30 +(* method invocation *)
    8.31 +
    8.32 +fun method name arg =
    8.33 +  let
    8.34 +    val id = new_id ();
    8.35 +    val promise = Future.promise () : string future;
    8.36 +    val _ = Synchronized.change promises (Symtab.update (id, promise));
    8.37 +    val _ = Output.raw_message (Markup.invoke_scala name id) arg;
    8.38 +  in promise end;
    8.39 +
    8.40 +
    8.41 +(* fulfill method *)
    8.42 +
    8.43 +exception Null;
    8.44 +
    8.45 +fun fulfill_method id tag res =
    8.46 +  let
    8.47 +    val result =
    8.48 +      (case tag of
    8.49 +        "0" => Exn.Exn Null
    8.50 +      | "1" => Exn.Result res
    8.51 +      | "2" => Exn.Exn (ERROR res)
    8.52 +      | "3" => Exn.Exn (Fail res)
    8.53 +      | _ => raise Fail "Bad tag");
    8.54 +    val promise =
    8.55 +      Synchronized.change_result promises
    8.56 +        (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
    8.57 +    val _ = Future.fulfill_result promise result;
    8.58 +  in () end;
    8.59 +
    8.60 +end;
    8.61 +
     9.1 --- a/src/Pure/System/invoke_scala.scala	Mon Jul 11 15:56:30 2011 +0200
     9.2 +++ b/src/Pure/System/invoke_scala.scala	Mon Jul 11 16:48:02 2011 +0200
     9.3 @@ -1,32 +1,62 @@
     9.4  /*  Title:      Pure/System/invoke_scala.scala
     9.5      Author:     Makarius
     9.6  
     9.7 -Invoke static methods (String)String via reflection.
     9.8 +JVM method invocation service via Scala layer.
     9.9  */
    9.10  
    9.11  package isabelle
    9.12  
    9.13  
    9.14  import java.lang.reflect.{Method, Modifier}
    9.15 +import scala.util.matching.Regex
    9.16  
    9.17  
    9.18  object Invoke_Scala
    9.19  {
    9.20 +  /* method reflection */
    9.21 +
    9.22 +  private val Ext = new Regex("(.*)\\.([^.]*)")
    9.23    private val STRING = Class.forName("java.lang.String")
    9.24  
    9.25 -  def method(class_name: String, method_name: String): String => String =
    9.26 +  private def get_method(name: String): String => String =
    9.27 +    name match {
    9.28 +      case Ext(class_name, method_name) =>
    9.29 +        val m =
    9.30 +          try { Class.forName(class_name).getMethod(method_name, STRING) }
    9.31 +          catch {
    9.32 +            case _: ClassNotFoundException =>
    9.33 +              error("Class not found: " + quote(class_name))
    9.34 +            case _: NoSuchMethodException =>
    9.35 +              error("No such method: " + quote(class_name + "." + method_name))
    9.36 +          }
    9.37 +        if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
    9.38 +        if (m.getReturnType != STRING) error("Bad return type of method: " + m.toString)
    9.39 +
    9.40 +        (arg: String) => m.invoke(null, arg).asInstanceOf[String]
    9.41 +      case _ => error("Malformed method name: " + quote(name))
    9.42 +    }
    9.43 +
    9.44 +
    9.45 +  /* method invocation */
    9.46 +
    9.47 +  object Tag extends Enumeration
    9.48    {
    9.49 -    val m =
    9.50 -      try { Class.forName(class_name).getMethod(method_name, STRING) }
    9.51 -      catch {
    9.52 -        case _: ClassNotFoundException =>
    9.53 -          error("Class not found: " + quote(class_name))
    9.54 -        case _: NoSuchMethodException =>
    9.55 -          error("No such method: " + quote(class_name + "." + method_name))
    9.56 -      }
    9.57 -    if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
    9.58 -    if (m.getReturnType != STRING) error("Bad return type of method: " + m.toString)
    9.59 +    val NULL = Value("0")
    9.60 +    val OK = Value("1")
    9.61 +    val ERROR = Value("2")
    9.62 +    val FAIL = Value("3")
    9.63 +  }
    9.64  
    9.65 -    (s: String) => m.invoke(null, s).asInstanceOf[String]
    9.66 -  }
    9.67 +  def method(name: String, arg: String): (Tag.Value, String) =
    9.68 +    Exn.capture { get_method(name) } match {
    9.69 +      case Exn.Res(f) =>
    9.70 +        Exn.capture { f(arg) } match {
    9.71 +          case Exn.Res(null) => (Tag.NULL, "")
    9.72 +          case Exn.Res(res) => (Tag.OK, res)
    9.73 +          case Exn.Exn(ERROR(msg)) => (Tag.ERROR, msg)
    9.74 +          case Exn.Exn(e) => throw e
    9.75 +        }
    9.76 +      case Exn.Exn(ERROR(msg)) => (Tag.FAIL, msg)
    9.77 +      case Exn.Exn(e) => throw e
    9.78 +    }
    9.79  }
    10.1 --- a/src/Pure/System/isabelle_process.scala	Mon Jul 11 15:56:30 2011 +0200
    10.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Jul 11 16:48:02 2011 +0200
    10.3 @@ -63,6 +63,7 @@
    10.4      {
    10.5        val res =
    10.6          if (is_status || is_report) message.body.map(_.toString).mkString
    10.7 +        else if (is_raw) "..."
    10.8          else Pretty.string_of(message.body)
    10.9        if (properties.isEmpty)
   10.10          kind.toString + " [[" + res + "]]"
    11.1 --- a/src/Pure/System/session.scala	Mon Jul 11 15:56:30 2011 +0200
    11.2 +++ b/src/Pure/System/session.scala	Mon Jul 11 16:48:02 2011 +0200
    11.3 @@ -255,12 +255,20 @@
    11.4        }
    11.5  
    11.6        result.properties match {
    11.7 -        case Position.Id(state_id) =>
    11.8 +        case Position.Id(state_id) if !result.is_raw =>
    11.9            try {
   11.10              val st = global_state.change_yield(_.accumulate(state_id, result.message))
   11.11              command_change_buffer ! st.command
   11.12            }
   11.13 -          catch { case _: Document.State.Fail => bad_result(result) }
   11.14 +          catch {
   11.15 +            case _: Document.State.Fail => bad_result(result)
   11.16 +          }
   11.17 +        case Markup.Invoke_Scala(name, id) if result.is_raw =>
   11.18 +          Future.fork {
   11.19 +            val arg = XML.content(result.body).mkString
   11.20 +            val (tag, res) = Invoke_Scala.method(name, arg)
   11.21 +            prover.get.invoke_scala(id, tag, res)
   11.22 +          }
   11.23          case _ =>
   11.24            if (result.is_syslog) {
   11.25              reverse_syslog ::= result.message
   11.26 @@ -289,9 +297,8 @@
   11.27                case _ => bad_result(result)
   11.28              }
   11.29            }
   11.30 -          else if (result.is_raw) { } // FIXME
   11.31            else bad_result(result)
   11.32 -        }
   11.33 +      }
   11.34      }
   11.35      //}}}
   11.36