--- 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 **)
--- 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)
--- 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);
--- 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 \
--- 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;
--- 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)
+ }
}
--- 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";
--- /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;
+
--- 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
+ }
}
--- 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 + "]]"
--- 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)
- }
+ }
}
//}}}