# HG changeset patch
# User wenzelm
# Date 1310397751 -7200
# Node ID 52310132063bc6c4cf48d592e7a43c3f14611c70
# Parent  17c36f05b40d03e1c3e12507fd93876ed9672485# Parent  0517a69de5d6e20e7decd6b72cdb5a405269e53e
merged

diff -r 17c36f05b40d -r 52310132063b NEWS
--- 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)
diff -r 17c36f05b40d -r 52310132063b src/Pure/General/markup.ML
--- 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 **)
 
diff -r 17c36f05b40d -r 52310132063b src/Pure/General/markup.scala
--- 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)
diff -r 17c36f05b40d -r 52310132063b src/Pure/General/output.ML
--- 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);
 
diff -r 17c36f05b40d -r 52310132063b src/Pure/General/xml.scala
--- 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
diff -r 17c36f05b40d -r 52310132063b src/Pure/General/yxml.scala
--- 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)
diff -r 17c36f05b40d -r 52310132063b src/Pure/IsaMakefile
--- 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					\
diff -r 17c36f05b40d -r 52310132063b src/Pure/PIDE/isar_document.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;
 
diff -r 17c36f05b40d -r 52310132063b src/Pure/PIDE/isar_document.scala
--- 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)
+  }
 }
diff -r 17c36f05b40d -r 52310132063b src/Pure/ROOT.ML
--- 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";
 
diff -r 17c36f05b40d -r 52310132063b 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 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;
+
diff -r 17c36f05b40d -r 52310132063b src/Pure/System/invoke_scala.scala
--- /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)
+    }
+}
diff -r 17c36f05b40d -r 52310132063b src/Pure/System/isabelle_process.ML
--- 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 ());
diff -r 17c36f05b40d -r 52310132063b src/Pure/System/isabelle_process.scala
--- 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 {
diff -r 17c36f05b40d -r 52310132063b src/Pure/System/session.scala
--- 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)
-        }
+      }
     }
     //}}}
 
diff -r 17c36f05b40d -r 52310132063b src/Pure/System/standard_system.scala
--- 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 */
 
diff -r 17c36f05b40d -r 52310132063b src/Pure/build-jars
--- 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
diff -r 17c36f05b40d -r 52310132063b src/Pure/library.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
       }
   }