# HG changeset patch
# User wenzelm
# Date 1310395682 -7200
# Node ID c70bd78ec83c38488b0702230f7753e778921c06
# Parent  74a9e9c8d5e85f2577994e0ff6f05cacdd508128
JVM method invocation service via Scala layer;

diff -r 74a9e9c8d5e8 -r c70bd78ec83c src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Mon Jul 11 15:56:30 2011 +0200
+++ b/src/Pure/General/markup.ML	Mon Jul 11 16:48:02 2011 +0200
@@ -117,6 +117,8 @@
   val reportN: string val report: T
   val no_reportN: string val no_report: T
   val badN: string val bad: T
+  val functionN: string
+  val invoke_scala: string -> string -> Properties.T
   val no_output: Output.output * Output.output
   val default_output: T -> Output.output * Output.output
   val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -368,6 +370,13 @@
 val (badN, bad) = markup_elem "bad";
 
 
+(* raw message functions *)
+
+val functionN = "function"
+
+fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
+
+
 
 (** print mode operations **)
 
diff -r 74a9e9c8d5e8 -r c70bd78ec83c src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Mon Jul 11 15:56:30 2011 +0200
+++ b/src/Pure/General/markup.scala	Mon Jul 11 16:48:02 2011 +0200
@@ -333,6 +333,22 @@
   val READY = "ready"
 
 
+  /* raw message functions */
+
+  val FUNCTION = "function"
+  val Function = new Property(FUNCTION)
+
+  val INVOKE_SCALA = "invoke_scala"
+  object Invoke_Scala
+  {
+    def unapply(props: List[(String, String)]): Option[(String, String)] =
+      props match {
+        case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
+        case _ => None
+      }
+  }
+
+
   /* system data */
 
   val Data = Markup("data", Nil)
diff -r 74a9e9c8d5e8 -r c70bd78ec83c src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Jul 11 15:56:30 2011 +0200
+++ b/src/Pure/General/output.ML	Mon Jul 11 16:48:02 2011 +0200
@@ -96,7 +96,9 @@
   val prompt_fn = Unsynchronized.ref raw_stdout;
   val status_fn = Unsynchronized.ref (fn _: output => ());
   val report_fn = Unsynchronized.ref (fn _: output => ());
-  val raw_message_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
+  val raw_message_fn =
+    Unsynchronized.ref
+      (fn _: Properties.T => fn _: output => raise Fail "Output.raw_message undefined");
 end;
 
 fun writeln s = ! Private_Hooks.writeln_fn (output s);
diff -r 74a9e9c8d5e8 -r c70bd78ec83c src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Mon Jul 11 15:56:30 2011 +0200
+++ b/src/Pure/IsaMakefile	Mon Jul 11 16:48:02 2011 +0200
@@ -189,6 +189,7 @@
   Syntax/syntax_phases.ML				\
   Syntax/syntax_trans.ML				\
   Syntax/term_position.ML				\
+  System/invoke_scala.ML				\
   System/isabelle_process.ML				\
   System/isabelle_system.ML				\
   System/isar.ML					\
diff -r 74a9e9c8d5e8 -r c70bd78ec83c src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Mon Jul 11 15:56:30 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Mon Jul 11 16:48:02 2011 +0200
@@ -33,5 +33,9 @@
       val state'' = Document.execute new_id state';
     in state'' end));
 
+val _ =
+  Isabelle_Process.add_command "Isar_Document.invoke_scala"
+    (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
+
 end;
 
diff -r 74a9e9c8d5e8 -r c70bd78ec83c src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Mon Jul 11 15:56:30 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Mon Jul 11 16:48:02 2011 +0200
@@ -154,4 +154,12 @@
       Document.ID(old_id), Document.ID(new_id),
         YXML.string_of_body(arg1), YXML.string_of_body(arg2))
   }
+
+
+  /* method invocation service */
+
+  def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
+  {
+    input("Isar_Document.invoke_scala", id, tag.toString, res)
+  }
 }
diff -r 74a9e9c8d5e8 -r c70bd78ec83c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Jul 11 15:56:30 2011 +0200
+++ b/src/Pure/ROOT.ML	Mon Jul 11 16:48:02 2011 +0200
@@ -274,6 +274,7 @@
 
 use "System/session.ML";
 use "System/isabelle_process.ML";
+use "System/invoke_scala.ML";
 use "PIDE/isar_document.ML";
 use "System/isar.ML";
 
diff -r 74a9e9c8d5e8 -r c70bd78ec83c src/Pure/System/invoke_scala.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/invoke_scala.ML	Mon Jul 11 16:48:02 2011 +0200
@@ -0,0 +1,58 @@
+(*  Title:      Pure/System/invoke_scala.ML
+    Author:     Makarius
+
+JVM method invocation service via Scala layer.
+
+TODO: proper cancellation!
+*)
+
+signature INVOKE_SCALA =
+sig
+  val method: string -> string -> string future
+  exception Null
+  val fulfill_method: string -> string -> string -> unit
+end;
+
+structure Invoke_Scala: INVOKE_SCALA =
+struct
+
+(* pending promises *)
+
+val new_id = string_of_int o Synchronized.counter ();
+
+val promises =
+  Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
+
+
+(* method invocation *)
+
+fun method name arg =
+  let
+    val id = new_id ();
+    val promise = Future.promise () : string future;
+    val _ = Synchronized.change promises (Symtab.update (id, promise));
+    val _ = Output.raw_message (Markup.invoke_scala name id) arg;
+  in promise end;
+
+
+(* fulfill method *)
+
+exception Null;
+
+fun fulfill_method id tag res =
+  let
+    val result =
+      (case tag of
+        "0" => Exn.Exn Null
+      | "1" => Exn.Result res
+      | "2" => Exn.Exn (ERROR res)
+      | "3" => Exn.Exn (Fail res)
+      | _ => raise Fail "Bad tag");
+    val promise =
+      Synchronized.change_result promises
+        (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
+    val _ = Future.fulfill_result promise result;
+  in () end;
+
+end;
+
diff -r 74a9e9c8d5e8 -r c70bd78ec83c src/Pure/System/invoke_scala.scala
--- a/src/Pure/System/invoke_scala.scala	Mon Jul 11 15:56:30 2011 +0200
+++ b/src/Pure/System/invoke_scala.scala	Mon Jul 11 16:48:02 2011 +0200
@@ -1,32 +1,62 @@
 /*  Title:      Pure/System/invoke_scala.scala
     Author:     Makarius
 
-Invoke static methods (String)String via reflection.
+JVM method invocation service via Scala layer.
 */
 
 package isabelle
 
 
 import java.lang.reflect.{Method, Modifier}
+import scala.util.matching.Regex
 
 
 object Invoke_Scala
 {
+  /* method reflection */
+
+  private val Ext = new Regex("(.*)\\.([^.]*)")
   private val STRING = Class.forName("java.lang.String")
 
-  def method(class_name: String, method_name: String): String => String =
+  private def get_method(name: String): String => String =
+    name match {
+      case Ext(class_name, method_name) =>
+        val m =
+          try { Class.forName(class_name).getMethod(method_name, STRING) }
+          catch {
+            case _: ClassNotFoundException =>
+              error("Class not found: " + quote(class_name))
+            case _: NoSuchMethodException =>
+              error("No such method: " + quote(class_name + "." + method_name))
+          }
+        if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
+        if (m.getReturnType != STRING) error("Bad return type of method: " + m.toString)
+
+        (arg: String) => m.invoke(null, arg).asInstanceOf[String]
+      case _ => error("Malformed method name: " + quote(name))
+    }
+
+
+  /* method invocation */
+
+  object Tag extends Enumeration
   {
-    val m =
-      try { Class.forName(class_name).getMethod(method_name, STRING) }
-      catch {
-        case _: ClassNotFoundException =>
-          error("Class not found: " + quote(class_name))
-        case _: NoSuchMethodException =>
-          error("No such method: " + quote(class_name + "." + method_name))
-      }
-    if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
-    if (m.getReturnType != STRING) error("Bad return type of method: " + m.toString)
+    val NULL = Value("0")
+    val OK = Value("1")
+    val ERROR = Value("2")
+    val FAIL = Value("3")
+  }
 
-    (s: String) => m.invoke(null, s).asInstanceOf[String]
-  }
+  def method(name: String, arg: String): (Tag.Value, String) =
+    Exn.capture { get_method(name) } match {
+      case Exn.Res(f) =>
+        Exn.capture { f(arg) } match {
+          case Exn.Res(null) => (Tag.NULL, "")
+          case Exn.Res(res) => (Tag.OK, res)
+          case Exn.Exn(ERROR(msg)) => (Tag.ERROR, msg)
+          case Exn.Exn(e) => throw e
+        }
+      case Exn.Exn(ERROR(msg)) => (Tag.FAIL, msg)
+      case Exn.Exn(e) => throw e
+    }
 }
diff -r 74a9e9c8d5e8 -r c70bd78ec83c src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Jul 11 15:56:30 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Jul 11 16:48:02 2011 +0200
@@ -63,6 +63,7 @@
     {
       val res =
         if (is_status || is_report) message.body.map(_.toString).mkString
+        else if (is_raw) "..."
         else Pretty.string_of(message.body)
       if (properties.isEmpty)
         kind.toString + " [[" + res + "]]"
diff -r 74a9e9c8d5e8 -r c70bd78ec83c src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Jul 11 15:56:30 2011 +0200
+++ b/src/Pure/System/session.scala	Mon Jul 11 16:48:02 2011 +0200
@@ -255,12 +255,20 @@
       }
 
       result.properties match {
-        case Position.Id(state_id) =>
+        case Position.Id(state_id) if !result.is_raw =>
           try {
             val st = global_state.change_yield(_.accumulate(state_id, result.message))
             command_change_buffer ! st.command
           }
-          catch { case _: Document.State.Fail => bad_result(result) }
+          catch {
+            case _: Document.State.Fail => bad_result(result)
+          }
+        case Markup.Invoke_Scala(name, id) if result.is_raw =>
+          Future.fork {
+            val arg = XML.content(result.body).mkString
+            val (tag, res) = Invoke_Scala.method(name, arg)
+            prover.get.invoke_scala(id, tag, res)
+          }
         case _ =>
           if (result.is_syslog) {
             reverse_syslog ::= result.message
@@ -289,9 +297,8 @@
               case _ => bad_result(result)
             }
           }
-          else if (result.is_raw) { } // FIXME
           else bad_result(result)
-        }
+      }
     }
     //}}}