--- a/NEWS Mon Jul 11 07:04:30 2011 +0200
+++ b/NEWS Mon Jul 11 17:22:31 2011 +0200
@@ -204,6 +204,12 @@
INCOMPATIBILITY, classical tactics and derived proof methods require
proper Proof.context.
+* Scala layer provides JVM method invocation service for static
+methods of type (String)String, see Invoke_Scala.method in ML.
+For example:
+
+ Invoke_Scala.method "java.lang.System.getProperty" "java.home"
+
New in Isabelle2011 (January 2011)
--- a/src/Pure/General/markup.ML Mon Jul 11 07:04:30 2011 +0200
+++ b/src/Pure/General/markup.ML Mon Jul 11 17:22:31 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 07:04:30 2011 +0200
+++ b/src/Pure/General/markup.scala Mon Jul 11 17:22:31 2011 +0200
@@ -321,6 +321,7 @@
val TRACING = "tracing"
val WARNING = "warning"
val ERROR = "error"
+ val RAW = "raw"
val SYSTEM = "system"
val STDOUT = "stdout"
val EXIT = "exit"
@@ -332,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 07:04:30 2011 +0200
+++ b/src/Pure/General/output.ML Mon Jul 11 17:22:31 2011 +0200
@@ -35,12 +35,14 @@
val prompt_fn: (output -> unit) Unsynchronized.ref
val status_fn: (output -> unit) Unsynchronized.ref
val report_fn: (output -> unit) Unsynchronized.ref
+ val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
end
val urgent_message: string -> unit
val error_msg: string -> unit
val prompt: string -> unit
val status: string -> unit
val report: string -> unit
+ val raw_message: Properties.T -> string -> unit
end;
structure Output: OUTPUT =
@@ -92,8 +94,11 @@
val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
val prompt_fn = Unsynchronized.ref raw_stdout;
- val status_fn = Unsynchronized.ref (fn _: string => ());
- val report_fn = Unsynchronized.ref (fn _: string => ());
+ 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 => raise Fail "Output.raw_message undefined");
end;
fun writeln s = ! Private_Hooks.writeln_fn (output s);
@@ -104,6 +109,7 @@
fun prompt s = ! Private_Hooks.prompt_fn (output s);
fun status s = ! Private_Hooks.status_fn (output s);
fun report s = ! Private_Hooks.report_fn (output s);
+fun raw_message props s = ! Private_Hooks.raw_message_fn props (output s);
fun legacy_feature s = warning ("Legacy feature! " ^ s);
--- a/src/Pure/General/xml.scala Mon Jul 11 07:04:30 2011 +0200
+++ b/src/Pure/General/xml.scala Mon Jul 11 17:22:31 2011 +0200
@@ -72,16 +72,19 @@
def content_stream(tree: Tree): Stream[String] =
tree match {
- case Elem(_, body) => body.toStream.flatten(content_stream(_))
+ case Elem(_, body) => content_stream(body)
case Text(content) => Stream(content)
}
+ def content_stream(body: Body): Stream[String] =
+ body.toStream.flatten(content_stream(_))
def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
+ def content(body: Body): Iterator[String] = content_stream(body).iterator
/* pipe-lined cache for partial sharing */
- class Cache(initial_size: Int)
+ class Cache(initial_size: Int = 131071, max_string: Int = 100)
{
private val cache_actor = actor
{
@@ -108,7 +111,9 @@
def cache_string(x: String): String =
lookup(x) match {
case Some(y) => y
- case None => store(trim_bytes(x))
+ case None =>
+ val z = trim_bytes(x)
+ if (z.length > max_string) z else store(z)
}
def cache_props(x: List[(String, String)]): List[(String, String)] =
if (x.isEmpty) x
--- a/src/Pure/General/yxml.scala Mon Jul 11 07:04:30 2011 +0200
+++ b/src/Pure/General/yxml.scala Mon Jul 11 17:22:31 2011 +0200
@@ -41,28 +41,6 @@
def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
- /* decoding pseudo UTF-8 */
-
- private class Decode_Chars(decode: String => String,
- buffer: Array[Byte], start: Int, end: Int) extends CharSequence
- {
- def length: Int = end - start
- def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
- def subSequence(i: Int, j: Int): CharSequence =
- new Decode_Chars(decode, buffer, start + i, start + j)
-
- // toString with adhoc decoding: abuse of CharSequence interface
- override def toString: String = decode(Standard_System.decode_permissive_utf8(this))
- }
-
- def decode_chars(decode: String => String,
- buffer: Array[Byte], start: Int, end: Int): CharSequence =
- {
- require(0 <= start && start <= end && end <= buffer.length)
- new Decode_Chars(decode, buffer, start, end)
- }
-
-
/* parsing */
private def err(msg: String) = error("Malformed YXML: " + msg)
--- a/src/Pure/IsaMakefile Mon Jul 11 07:04:30 2011 +0200
+++ b/src/Pure/IsaMakefile Mon Jul 11 17:22:31 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 07:04:30 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML Mon Jul 11 17:22:31 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 07:04:30 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala Mon Jul 11 17:22:31 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 07:04:30 2011 +0200
+++ b/src/Pure/ROOT.ML Mon Jul 11 17:22:31 2011 +0200
@@ -27,9 +27,9 @@
if Multithreading.available then ()
else use "Concurrent/synchronized_sequential.ML";
+use "General/properties.ML";
use "General/output.ML";
use "General/timing.ML";
-use "General/properties.ML";
use "General/markup.ML";
use "General/scan.ML";
use "General/source.ML";
@@ -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 17:22:31 2011 +0200
@@ -0,0 +1,62 @@
+(* Title: Pure/System/invoke_scala.ML
+ Author: Makarius
+
+JVM method invocation service via Scala layer.
+
+TODO: proper cancellation!
+*)
+
+signature INVOKE_SCALA =
+sig
+ exception Null
+ val method: string -> string -> string
+ val promise_method: string -> string -> string future
+ val fulfill_method: string -> string -> string -> unit
+end;
+
+structure Invoke_Scala: INVOKE_SCALA =
+struct
+
+exception Null;
+
+
+(* 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 promise_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;
+
+fun method name arg = Future.join (promise_method name arg);
+
+
+(* fulfill method *)
+
+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;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/invoke_scala.scala Mon Jul 11 17:22:31 2011 +0200
@@ -0,0 +1,66 @@
+/* Title: Pure/System/invoke_scala.scala
+ Author: Makarius
+
+JVM method invocation service via Scala layer.
+*/
+
+package isabelle
+
+
+import java.lang.reflect.{Method, Modifier, InvocationTargetException}
+import scala.util.matching.Regex
+
+
+object Invoke_Scala
+{
+ /* method reflection */
+
+ private val Ext = new Regex("(.*)\\.([^.]*)")
+ private val STRING = Class.forName("java.lang.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 | _: NoSuchMethodException =>
+ error("No such method: " + quote(name))
+ }
+ if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
+ if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
+
+ (arg: String) => {
+ try { m.invoke(null, arg).asInstanceOf[String] }
+ catch {
+ case e: InvocationTargetException if e.getCause != null =>
+ throw e.getCause
+ }
+ }
+ case _ => error("Malformed method name: " + quote(name))
+ }
+
+
+ /* method invocation */
+
+ object Tag extends Enumeration
+ {
+ val NULL = Value("0")
+ val OK = Value("1")
+ val ERROR = Value("2")
+ val FAIL = Value("3")
+ }
+
+ 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) => (Tag.ERROR, e.toString)
+ }
+ case Exn.Exn(ERROR(msg)) => (Tag.FAIL, msg)
+ case Exn.Exn(e) => (Tag.FAIL, e.toString)
+ }
+}
--- a/src/Pure/System/isabelle_process.ML Mon Jul 11 07:04:30 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML Mon Jul 11 17:22:31 2011 +0200
@@ -108,6 +108,7 @@
Output.Private_Hooks.tracing_fn := standard_message mbox true "E";
Output.Private_Hooks.warning_fn := standard_message mbox true "F";
Output.Private_Hooks.error_fn := standard_message mbox true "G";
+ Output.Private_Hooks.raw_message_fn := message mbox "H";
Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
Output.Private_Hooks.prompt_fn := ignore;
message mbox "A" [] (Session.welcome ());
--- a/src/Pure/System/isabelle_process.scala Mon Jul 11 07:04:30 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala Mon Jul 11 17:22:31 2011 +0200
@@ -29,7 +29,8 @@
('D' : Int) -> Markup.WRITELN,
('E' : Int) -> Markup.TRACING,
('F' : Int) -> Markup.WARNING,
- ('G' : Int) -> Markup.ERROR)
+ ('G' : Int) -> Markup.ERROR,
+ ('H' : Int) -> Markup.RAW)
}
abstract class Message
@@ -44,9 +45,9 @@
class Result(val message: XML.Elem) extends Message
{
- def kind = message.markup.name
- def properties = message.markup.properties
- def body = message.body
+ def kind: String = message.markup.name
+ def properties: XML.Attributes = message.markup.properties
+ def body: XML.Body = message.body
def is_init = kind == Markup.INIT
def is_exit = kind == Markup.EXIT
@@ -54,6 +55,7 @@
def is_system = kind == Markup.SYSTEM
def is_status = kind == Markup.STATUS
def is_report = kind == Markup.REPORT
+ def is_raw = kind == Markup.RAW
def is_ready = Isar_Document.is_ready(message)
def is_syslog = is_init || is_exit || is_system || is_ready
@@ -61,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 + "]]"
@@ -90,14 +93,18 @@
receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
}
- private val xml_cache = new XML.Cache(131071)
+ private val xml_cache = new XML.Cache()
private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
{
if (kind == Markup.INIT) rm_fifos()
- val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
- xml_cache.cache_tree(msg)((message: XML.Tree) =>
- receiver ! new Result(message.asInstanceOf[XML.Elem]))
+ if (kind == Markup.RAW)
+ receiver ! new Result(XML.Elem(Markup(kind, props), body))
+ else {
+ val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
+ xml_cache.cache_tree(msg)((message: XML.Tree) =>
+ receiver ! new Result(message.asInstanceOf[XML.Elem]))
+ }
}
private def put_result(kind: String, text: String)
@@ -324,7 +331,7 @@
val default_buffer = new Array[Byte](65536)
var c = -1
- def read_chunk(): XML.Body =
+ def read_chunk(decode: Boolean): XML.Body =
{
//{{{
// chunk size
@@ -351,19 +358,24 @@
if (i != n) throw new Protocol_Error("bad message chunk content")
- YXML.parse_body_failsafe(YXML.decode_chars(Symbol.decode, buf, 0, n))
+ if (decode)
+ YXML.parse_body_failsafe(Standard_System.decode_chars(Symbol.decode, buf, 0, n))
+ else List(XML.Text(Standard_System.decode_chars(s => s, buf, 0, n).toString))
//}}}
}
do {
try {
- val header = read_chunk()
- val body = read_chunk()
+ val header = read_chunk(true)
header match {
case List(XML.Elem(Markup(name, props), Nil))
if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
- put_result(Kind.message_markup(name(0)), props, body)
- case _ => throw new Protocol_Error("bad header: " + header.toString)
+ val kind = Kind.message_markup(name(0))
+ val body = read_chunk(kind != Markup.RAW)
+ put_result(kind, props, body)
+ case _ =>
+ read_chunk(false)
+ throw new Protocol_Error("bad header: " + header.toString)
}
}
catch {
--- a/src/Pure/System/session.scala Mon Jul 11 07:04:30 2011 +0200
+++ b/src/Pure/System/session.scala Mon Jul 11 17:22:31 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
@@ -290,7 +298,7 @@
}
}
else bad_result(result)
- }
+ }
}
//}}}
--- a/src/Pure/System/standard_system.scala Mon Jul 11 07:04:30 2011 +0200
+++ b/src/Pure/System/standard_system.scala Mon Jul 11 17:22:31 2011 +0200
@@ -79,6 +79,25 @@
buf.toString
}
+ private class Decode_Chars(decode: String => String,
+ buffer: Array[Byte], start: Int, end: Int) extends CharSequence
+ {
+ def length: Int = end - start
+ def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
+ def subSequence(i: Int, j: Int): CharSequence =
+ new Decode_Chars(decode, buffer, start + i, start + j)
+
+ // toString with adhoc decoding: abuse of CharSequence interface
+ override def toString: String = decode(decode_permissive_utf8(this))
+ }
+
+ def decode_chars(decode: String => String,
+ buffer: Array[Byte], start: Int, end: Int): CharSequence =
+ {
+ require(0 <= start && start <= end && end <= buffer.length)
+ new Decode_Chars(decode, buffer, start, end)
+ }
+
/* basic file operations */
--- a/src/Pure/build-jars Mon Jul 11 07:04:30 2011 +0200
+++ b/src/Pure/build-jars Mon Jul 11 17:22:31 2011 +0200
@@ -40,6 +40,7 @@
System/download.scala
System/event_bus.scala
System/gui_setup.scala
+ System/invoke_scala.scala
System/isabelle_charset.scala
System/isabelle_process.scala
System/isabelle_syntax.scala
--- a/src/Pure/library.scala Mon Jul 11 07:04:30 2011 +0200
+++ b/src/Pure/library.scala Mon Jul 11 17:22:31 2011 +0200
@@ -27,7 +27,7 @@
exn match {
case e: RuntimeException =>
val msg = e.getMessage
- Some(if (msg == null) "" else msg)
+ Some(if (msg == null) "Error" else msg)
case _ => None
}
}