merged
authorwenzelm
Mon Jul 11 17:22:31 2011 +0200 (2011-07-11)
changeset 4375852310132063b
parent 43757 17c36f05b40d
parent 43752 0517a69de5d6
child 43759 d93a69672362
child 43764 366d5726de09
merged
     1.1 --- a/NEWS	Mon Jul 11 07:04:30 2011 +0200
     1.2 +++ b/NEWS	Mon Jul 11 17:22:31 2011 +0200
     1.3 @@ -204,6 +204,12 @@
     1.4  INCOMPATIBILITY, classical tactics and derived proof methods require
     1.5  proper Proof.context.
     1.6  
     1.7 +* Scala layer provides JVM method invocation service for static
     1.8 +methods of type (String)String, see Invoke_Scala.method in ML.
     1.9 +For example:
    1.10 +
    1.11 +  Invoke_Scala.method "java.lang.System.getProperty" "java.home"
    1.12 +
    1.13  
    1.14  
    1.15  New in Isabelle2011 (January 2011)
     2.1 --- a/src/Pure/General/markup.ML	Mon Jul 11 07:04:30 2011 +0200
     2.2 +++ b/src/Pure/General/markup.ML	Mon Jul 11 17:22:31 2011 +0200
     2.3 @@ -117,6 +117,8 @@
     2.4    val reportN: string val report: T
     2.5    val no_reportN: string val no_report: T
     2.6    val badN: string val bad: T
     2.7 +  val functionN: string
     2.8 +  val invoke_scala: string -> string -> Properties.T
     2.9    val no_output: Output.output * Output.output
    2.10    val default_output: T -> Output.output * Output.output
    2.11    val add_mode: string -> (T -> Output.output * Output.output) -> unit
    2.12 @@ -368,6 +370,13 @@
    2.13  val (badN, bad) = markup_elem "bad";
    2.14  
    2.15  
    2.16 +(* raw message functions *)
    2.17 +
    2.18 +val functionN = "function"
    2.19 +
    2.20 +fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
    2.21 +
    2.22 +
    2.23  
    2.24  (** print mode operations **)
    2.25  
     3.1 --- a/src/Pure/General/markup.scala	Mon Jul 11 07:04:30 2011 +0200
     3.2 +++ b/src/Pure/General/markup.scala	Mon Jul 11 17:22:31 2011 +0200
     3.3 @@ -321,6 +321,7 @@
     3.4    val TRACING = "tracing"
     3.5    val WARNING = "warning"
     3.6    val ERROR = "error"
     3.7 +  val RAW = "raw"
     3.8    val SYSTEM = "system"
     3.9    val STDOUT = "stdout"
    3.10    val EXIT = "exit"
    3.11 @@ -332,6 +333,22 @@
    3.12    val READY = "ready"
    3.13  
    3.14  
    3.15 +  /* raw message functions */
    3.16 +
    3.17 +  val FUNCTION = "function"
    3.18 +  val Function = new Property(FUNCTION)
    3.19 +
    3.20 +  val INVOKE_SCALA = "invoke_scala"
    3.21 +  object Invoke_Scala
    3.22 +  {
    3.23 +    def unapply(props: List[(String, String)]): Option[(String, String)] =
    3.24 +      props match {
    3.25 +        case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
    3.26 +        case _ => None
    3.27 +      }
    3.28 +  }
    3.29 +
    3.30 +
    3.31    /* system data */
    3.32  
    3.33    val Data = Markup("data", Nil)
     4.1 --- a/src/Pure/General/output.ML	Mon Jul 11 07:04:30 2011 +0200
     4.2 +++ b/src/Pure/General/output.ML	Mon Jul 11 17:22:31 2011 +0200
     4.3 @@ -35,12 +35,14 @@
     4.4      val prompt_fn: (output -> unit) Unsynchronized.ref
     4.5      val status_fn: (output -> unit) Unsynchronized.ref
     4.6      val report_fn: (output -> unit) Unsynchronized.ref
     4.7 +    val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
     4.8    end
     4.9    val urgent_message: string -> unit
    4.10    val error_msg: string -> unit
    4.11    val prompt: string -> unit
    4.12    val status: string -> unit
    4.13    val report: string -> unit
    4.14 +  val raw_message: Properties.T -> string -> unit
    4.15  end;
    4.16  
    4.17  structure Output: OUTPUT =
    4.18 @@ -92,8 +94,11 @@
    4.19    val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
    4.20    val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
    4.21    val prompt_fn = Unsynchronized.ref raw_stdout;
    4.22 -  val status_fn = Unsynchronized.ref (fn _: string => ());
    4.23 -  val report_fn = Unsynchronized.ref (fn _: string => ());
    4.24 +  val status_fn = Unsynchronized.ref (fn _: output => ());
    4.25 +  val report_fn = Unsynchronized.ref (fn _: output => ());
    4.26 +  val raw_message_fn =
    4.27 +    Unsynchronized.ref
    4.28 +      (fn _: Properties.T => fn _: output => raise Fail "Output.raw_message undefined");
    4.29  end;
    4.30  
    4.31  fun writeln s = ! Private_Hooks.writeln_fn (output s);
    4.32 @@ -104,6 +109,7 @@
    4.33  fun prompt s = ! Private_Hooks.prompt_fn (output s);
    4.34  fun status s = ! Private_Hooks.status_fn (output s);
    4.35  fun report s = ! Private_Hooks.report_fn (output s);
    4.36 +fun raw_message props s = ! Private_Hooks.raw_message_fn props (output s);
    4.37  
    4.38  fun legacy_feature s = warning ("Legacy feature! " ^ s);
    4.39  
     5.1 --- a/src/Pure/General/xml.scala	Mon Jul 11 07:04:30 2011 +0200
     5.2 +++ b/src/Pure/General/xml.scala	Mon Jul 11 17:22:31 2011 +0200
     5.3 @@ -72,16 +72,19 @@
     5.4  
     5.5    def content_stream(tree: Tree): Stream[String] =
     5.6      tree match {
     5.7 -      case Elem(_, body) => body.toStream.flatten(content_stream(_))
     5.8 +      case Elem(_, body) => content_stream(body)
     5.9        case Text(content) => Stream(content)
    5.10      }
    5.11 +  def content_stream(body: Body): Stream[String] =
    5.12 +    body.toStream.flatten(content_stream(_))
    5.13  
    5.14    def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
    5.15 +  def content(body: Body): Iterator[String] = content_stream(body).iterator
    5.16  
    5.17  
    5.18    /* pipe-lined cache for partial sharing */
    5.19  
    5.20 -  class Cache(initial_size: Int)
    5.21 +  class Cache(initial_size: Int = 131071, max_string: Int = 100)
    5.22    {
    5.23      private val cache_actor = actor
    5.24      {
    5.25 @@ -108,7 +111,9 @@
    5.26        def cache_string(x: String): String =
    5.27          lookup(x) match {
    5.28            case Some(y) => y
    5.29 -          case None => store(trim_bytes(x))
    5.30 +          case None =>
    5.31 +            val z = trim_bytes(x)
    5.32 +            if (z.length > max_string) z else store(z)
    5.33          }
    5.34        def cache_props(x: List[(String, String)]): List[(String, String)] =
    5.35          if (x.isEmpty) x
     6.1 --- a/src/Pure/General/yxml.scala	Mon Jul 11 07:04:30 2011 +0200
     6.2 +++ b/src/Pure/General/yxml.scala	Mon Jul 11 17:22:31 2011 +0200
     6.3 @@ -41,28 +41,6 @@
     6.4    def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
     6.5  
     6.6  
     6.7 -  /* decoding pseudo UTF-8 */
     6.8 -
     6.9 -  private class Decode_Chars(decode: String => String,
    6.10 -    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
    6.11 -  {
    6.12 -    def length: Int = end - start
    6.13 -    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
    6.14 -    def subSequence(i: Int, j: Int): CharSequence =
    6.15 -      new Decode_Chars(decode, buffer, start + i, start + j)
    6.16 -
    6.17 -    // toString with adhoc decoding: abuse of CharSequence interface
    6.18 -    override def toString: String = decode(Standard_System.decode_permissive_utf8(this))
    6.19 -  }
    6.20 -
    6.21 -  def decode_chars(decode: String => String,
    6.22 -    buffer: Array[Byte], start: Int, end: Int): CharSequence =
    6.23 -  {
    6.24 -    require(0 <= start && start <= end && end <= buffer.length)
    6.25 -    new Decode_Chars(decode, buffer, start, end)
    6.26 -  }
    6.27 -
    6.28 -
    6.29    /* parsing */
    6.30  
    6.31    private def err(msg: String) = error("Malformed YXML: " + msg)
     7.1 --- a/src/Pure/IsaMakefile	Mon Jul 11 07:04:30 2011 +0200
     7.2 +++ b/src/Pure/IsaMakefile	Mon Jul 11 17:22:31 2011 +0200
     7.3 @@ -189,6 +189,7 @@
     7.4    Syntax/syntax_phases.ML				\
     7.5    Syntax/syntax_trans.ML				\
     7.6    Syntax/term_position.ML				\
     7.7 +  System/invoke_scala.ML				\
     7.8    System/isabelle_process.ML				\
     7.9    System/isabelle_system.ML				\
    7.10    System/isar.ML					\
     8.1 --- a/src/Pure/PIDE/isar_document.ML	Mon Jul 11 07:04:30 2011 +0200
     8.2 +++ b/src/Pure/PIDE/isar_document.ML	Mon Jul 11 17:22:31 2011 +0200
     8.3 @@ -33,5 +33,9 @@
     8.4        val state'' = Document.execute new_id state';
     8.5      in state'' end));
     8.6  
     8.7 +val _ =
     8.8 +  Isabelle_Process.add_command "Isar_Document.invoke_scala"
     8.9 +    (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
    8.10 +
    8.11  end;
    8.12  
     9.1 --- a/src/Pure/PIDE/isar_document.scala	Mon Jul 11 07:04:30 2011 +0200
     9.2 +++ b/src/Pure/PIDE/isar_document.scala	Mon Jul 11 17:22:31 2011 +0200
     9.3 @@ -154,4 +154,12 @@
     9.4        Document.ID(old_id), Document.ID(new_id),
     9.5          YXML.string_of_body(arg1), YXML.string_of_body(arg2))
     9.6    }
     9.7 +
     9.8 +
     9.9 +  /* method invocation service */
    9.10 +
    9.11 +  def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
    9.12 +  {
    9.13 +    input("Isar_Document.invoke_scala", id, tag.toString, res)
    9.14 +  }
    9.15  }
    10.1 --- a/src/Pure/ROOT.ML	Mon Jul 11 07:04:30 2011 +0200
    10.2 +++ b/src/Pure/ROOT.ML	Mon Jul 11 17:22:31 2011 +0200
    10.3 @@ -27,9 +27,9 @@
    10.4  if Multithreading.available then ()
    10.5  else use "Concurrent/synchronized_sequential.ML";
    10.6  
    10.7 +use "General/properties.ML";
    10.8  use "General/output.ML";
    10.9  use "General/timing.ML";
   10.10 -use "General/properties.ML";
   10.11  use "General/markup.ML";
   10.12  use "General/scan.ML";
   10.13  use "General/source.ML";
   10.14 @@ -274,6 +274,7 @@
   10.15  
   10.16  use "System/session.ML";
   10.17  use "System/isabelle_process.ML";
   10.18 +use "System/invoke_scala.ML";
   10.19  use "PIDE/isar_document.ML";
   10.20  use "System/isar.ML";
   10.21  
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Pure/System/invoke_scala.ML	Mon Jul 11 17:22:31 2011 +0200
    11.3 @@ -0,0 +1,62 @@
    11.4 +(*  Title:      Pure/System/invoke_scala.ML
    11.5 +    Author:     Makarius
    11.6 +
    11.7 +JVM method invocation service via Scala layer.
    11.8 +
    11.9 +TODO: proper cancellation!
   11.10 +*)
   11.11 +
   11.12 +signature INVOKE_SCALA =
   11.13 +sig
   11.14 +  exception Null
   11.15 +  val method: string -> string -> string
   11.16 +  val promise_method: string -> string -> string future
   11.17 +  val fulfill_method: string -> string -> string -> unit
   11.18 +end;
   11.19 +
   11.20 +structure Invoke_Scala: INVOKE_SCALA =
   11.21 +struct
   11.22 +
   11.23 +exception Null;
   11.24 +
   11.25 +
   11.26 +(* pending promises *)
   11.27 +
   11.28 +val new_id = string_of_int o Synchronized.counter ();
   11.29 +
   11.30 +val promises =
   11.31 +  Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
   11.32 +
   11.33 +
   11.34 +(* method invocation *)
   11.35 +
   11.36 +fun promise_method name arg =
   11.37 +  let
   11.38 +    val id = new_id ();
   11.39 +    val promise = Future.promise () : string future;
   11.40 +    val _ = Synchronized.change promises (Symtab.update (id, promise));
   11.41 +    val _ = Output.raw_message (Markup.invoke_scala name id) arg;
   11.42 +  in promise end;
   11.43 +
   11.44 +fun method name arg = Future.join (promise_method name arg);
   11.45 +
   11.46 +
   11.47 +(* fulfill method *)
   11.48 +
   11.49 +fun fulfill_method id tag res =
   11.50 +  let
   11.51 +    val result =
   11.52 +      (case tag of
   11.53 +        "0" => Exn.Exn Null
   11.54 +      | "1" => Exn.Result res
   11.55 +      | "2" => Exn.Exn (ERROR res)
   11.56 +      | "3" => Exn.Exn (Fail res)
   11.57 +      | _ => raise Fail "Bad tag");
   11.58 +    val promise =
   11.59 +      Synchronized.change_result promises
   11.60 +        (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
   11.61 +    val _ = Future.fulfill_result promise result;
   11.62 +  in () end;
   11.63 +
   11.64 +end;
   11.65 +
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Pure/System/invoke_scala.scala	Mon Jul 11 17:22:31 2011 +0200
    12.3 @@ -0,0 +1,66 @@
    12.4 +/*  Title:      Pure/System/invoke_scala.scala
    12.5 +    Author:     Makarius
    12.6 +
    12.7 +JVM method invocation service via Scala layer.
    12.8 +*/
    12.9 +
   12.10 +package isabelle
   12.11 +
   12.12 +
   12.13 +import java.lang.reflect.{Method, Modifier, InvocationTargetException}
   12.14 +import scala.util.matching.Regex
   12.15 +
   12.16 +
   12.17 +object Invoke_Scala
   12.18 +{
   12.19 +  /* method reflection */
   12.20 +
   12.21 +  private val Ext = new Regex("(.*)\\.([^.]*)")
   12.22 +  private val STRING = Class.forName("java.lang.String")
   12.23 +
   12.24 +  private def get_method(name: String): String => String =
   12.25 +    name match {
   12.26 +      case Ext(class_name, method_name) =>
   12.27 +        val m =
   12.28 +          try { Class.forName(class_name).getMethod(method_name, STRING) }
   12.29 +          catch {
   12.30 +            case _: ClassNotFoundException | _: NoSuchMethodException =>
   12.31 +              error("No such method: " + quote(name))
   12.32 +          }
   12.33 +        if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
   12.34 +        if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
   12.35 +
   12.36 +        (arg: String) => {
   12.37 +          try { m.invoke(null, arg).asInstanceOf[String] }
   12.38 +          catch {
   12.39 +            case e: InvocationTargetException if e.getCause != null =>
   12.40 +              throw e.getCause
   12.41 +          }
   12.42 +        }
   12.43 +      case _ => error("Malformed method name: " + quote(name))
   12.44 +    }
   12.45 +
   12.46 +
   12.47 +  /* method invocation */
   12.48 +
   12.49 +  object Tag extends Enumeration
   12.50 +  {
   12.51 +    val NULL = Value("0")
   12.52 +    val OK = Value("1")
   12.53 +    val ERROR = Value("2")
   12.54 +    val FAIL = Value("3")
   12.55 +  }
   12.56 +
   12.57 +  def method(name: String, arg: String): (Tag.Value, String) =
   12.58 +    Exn.capture { get_method(name) } match {
   12.59 +      case Exn.Res(f) =>
   12.60 +        Exn.capture { f(arg) } match {
   12.61 +          case Exn.Res(null) => (Tag.NULL, "")
   12.62 +          case Exn.Res(res) => (Tag.OK, res)
   12.63 +          case Exn.Exn(ERROR(msg)) => (Tag.ERROR, msg)
   12.64 +          case Exn.Exn(e) => (Tag.ERROR, e.toString)
   12.65 +        }
   12.66 +      case Exn.Exn(ERROR(msg)) => (Tag.FAIL, msg)
   12.67 +      case Exn.Exn(e) => (Tag.FAIL, e.toString)
   12.68 +    }
   12.69 +}
    13.1 --- a/src/Pure/System/isabelle_process.ML	Mon Jul 11 07:04:30 2011 +0200
    13.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Jul 11 17:22:31 2011 +0200
    13.3 @@ -108,6 +108,7 @@
    13.4      Output.Private_Hooks.tracing_fn := standard_message mbox true "E";
    13.5      Output.Private_Hooks.warning_fn := standard_message mbox true "F";
    13.6      Output.Private_Hooks.error_fn := standard_message mbox true "G";
    13.7 +    Output.Private_Hooks.raw_message_fn := message mbox "H";
    13.8      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    13.9      Output.Private_Hooks.prompt_fn := ignore;
   13.10      message mbox "A" [] (Session.welcome ());
    14.1 --- a/src/Pure/System/isabelle_process.scala	Mon Jul 11 07:04:30 2011 +0200
    14.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Jul 11 17:22:31 2011 +0200
    14.3 @@ -29,7 +29,8 @@
    14.4        ('D' : Int) -> Markup.WRITELN,
    14.5        ('E' : Int) -> Markup.TRACING,
    14.6        ('F' : Int) -> Markup.WARNING,
    14.7 -      ('G' : Int) -> Markup.ERROR)
    14.8 +      ('G' : Int) -> Markup.ERROR,
    14.9 +      ('H' : Int) -> Markup.RAW)
   14.10    }
   14.11  
   14.12    abstract class Message
   14.13 @@ -44,9 +45,9 @@
   14.14  
   14.15    class Result(val message: XML.Elem) extends Message
   14.16    {
   14.17 -    def kind = message.markup.name
   14.18 -    def properties = message.markup.properties
   14.19 -    def body = message.body
   14.20 +    def kind: String = message.markup.name
   14.21 +    def properties: XML.Attributes = message.markup.properties
   14.22 +    def body: XML.Body = message.body
   14.23  
   14.24      def is_init = kind == Markup.INIT
   14.25      def is_exit = kind == Markup.EXIT
   14.26 @@ -54,6 +55,7 @@
   14.27      def is_system = kind == Markup.SYSTEM
   14.28      def is_status = kind == Markup.STATUS
   14.29      def is_report = kind == Markup.REPORT
   14.30 +    def is_raw = kind == Markup.RAW
   14.31      def is_ready = Isar_Document.is_ready(message)
   14.32      def is_syslog = is_init || is_exit || is_system || is_ready
   14.33  
   14.34 @@ -61,6 +63,7 @@
   14.35      {
   14.36        val res =
   14.37          if (is_status || is_report) message.body.map(_.toString).mkString
   14.38 +        else if (is_raw) "..."
   14.39          else Pretty.string_of(message.body)
   14.40        if (properties.isEmpty)
   14.41          kind.toString + " [[" + res + "]]"
   14.42 @@ -90,14 +93,18 @@
   14.43      receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
   14.44    }
   14.45  
   14.46 -  private val xml_cache = new XML.Cache(131071)
   14.47 +  private val xml_cache = new XML.Cache()
   14.48  
   14.49    private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
   14.50    {
   14.51      if (kind == Markup.INIT) rm_fifos()
   14.52 -    val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
   14.53 -    xml_cache.cache_tree(msg)((message: XML.Tree) =>
   14.54 -      receiver ! new Result(message.asInstanceOf[XML.Elem]))
   14.55 +    if (kind == Markup.RAW)
   14.56 +      receiver ! new Result(XML.Elem(Markup(kind, props), body))
   14.57 +    else {
   14.58 +      val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
   14.59 +      xml_cache.cache_tree(msg)((message: XML.Tree) =>
   14.60 +        receiver ! new Result(message.asInstanceOf[XML.Elem]))
   14.61 +    }
   14.62    }
   14.63  
   14.64    private def put_result(kind: String, text: String)
   14.65 @@ -324,7 +331,7 @@
   14.66        val default_buffer = new Array[Byte](65536)
   14.67        var c = -1
   14.68  
   14.69 -      def read_chunk(): XML.Body =
   14.70 +      def read_chunk(decode: Boolean): XML.Body =
   14.71        {
   14.72          //{{{
   14.73          // chunk size
   14.74 @@ -351,19 +358,24 @@
   14.75  
   14.76          if (i != n) throw new Protocol_Error("bad message chunk content")
   14.77  
   14.78 -        YXML.parse_body_failsafe(YXML.decode_chars(Symbol.decode, buf, 0, n))
   14.79 +        if (decode)
   14.80 +          YXML.parse_body_failsafe(Standard_System.decode_chars(Symbol.decode, buf, 0, n))
   14.81 +        else List(XML.Text(Standard_System.decode_chars(s => s, buf, 0, n).toString))
   14.82          //}}}
   14.83        }
   14.84  
   14.85        do {
   14.86          try {
   14.87 -          val header = read_chunk()
   14.88 -          val body = read_chunk()
   14.89 +          val header = read_chunk(true)
   14.90            header match {
   14.91              case List(XML.Elem(Markup(name, props), Nil))
   14.92                  if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
   14.93 -              put_result(Kind.message_markup(name(0)), props, body)
   14.94 -            case _ => throw new Protocol_Error("bad header: " + header.toString)
   14.95 +              val kind = Kind.message_markup(name(0))
   14.96 +              val body = read_chunk(kind != Markup.RAW)
   14.97 +              put_result(kind, props, body)
   14.98 +            case _ =>
   14.99 +              read_chunk(false)
  14.100 +              throw new Protocol_Error("bad header: " + header.toString)
  14.101            }
  14.102          }
  14.103          catch {
    15.1 --- a/src/Pure/System/session.scala	Mon Jul 11 07:04:30 2011 +0200
    15.2 +++ b/src/Pure/System/session.scala	Mon Jul 11 17:22:31 2011 +0200
    15.3 @@ -255,12 +255,20 @@
    15.4        }
    15.5  
    15.6        result.properties match {
    15.7 -        case Position.Id(state_id) =>
    15.8 +        case Position.Id(state_id) if !result.is_raw =>
    15.9            try {
   15.10              val st = global_state.change_yield(_.accumulate(state_id, result.message))
   15.11              command_change_buffer ! st.command
   15.12            }
   15.13 -          catch { case _: Document.State.Fail => bad_result(result) }
   15.14 +          catch {
   15.15 +            case _: Document.State.Fail => bad_result(result)
   15.16 +          }
   15.17 +        case Markup.Invoke_Scala(name, id) if result.is_raw =>
   15.18 +          Future.fork {
   15.19 +            val arg = XML.content(result.body).mkString
   15.20 +            val (tag, res) = Invoke_Scala.method(name, arg)
   15.21 +            prover.get.invoke_scala(id, tag, res)
   15.22 +          }
   15.23          case _ =>
   15.24            if (result.is_syslog) {
   15.25              reverse_syslog ::= result.message
   15.26 @@ -290,7 +298,7 @@
   15.27              }
   15.28            }
   15.29            else bad_result(result)
   15.30 -        }
   15.31 +      }
   15.32      }
   15.33      //}}}
   15.34  
    16.1 --- a/src/Pure/System/standard_system.scala	Mon Jul 11 07:04:30 2011 +0200
    16.2 +++ b/src/Pure/System/standard_system.scala	Mon Jul 11 17:22:31 2011 +0200
    16.3 @@ -79,6 +79,25 @@
    16.4      buf.toString
    16.5    }
    16.6  
    16.7 +  private class Decode_Chars(decode: String => String,
    16.8 +    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
    16.9 +  {
   16.10 +    def length: Int = end - start
   16.11 +    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
   16.12 +    def subSequence(i: Int, j: Int): CharSequence =
   16.13 +      new Decode_Chars(decode, buffer, start + i, start + j)
   16.14 +
   16.15 +    // toString with adhoc decoding: abuse of CharSequence interface
   16.16 +    override def toString: String = decode(decode_permissive_utf8(this))
   16.17 +  }
   16.18 +
   16.19 +  def decode_chars(decode: String => String,
   16.20 +    buffer: Array[Byte], start: Int, end: Int): CharSequence =
   16.21 +  {
   16.22 +    require(0 <= start && start <= end && end <= buffer.length)
   16.23 +    new Decode_Chars(decode, buffer, start, end)
   16.24 +  }
   16.25 +
   16.26  
   16.27    /* basic file operations */
   16.28  
    17.1 --- a/src/Pure/build-jars	Mon Jul 11 07:04:30 2011 +0200
    17.2 +++ b/src/Pure/build-jars	Mon Jul 11 17:22:31 2011 +0200
    17.3 @@ -40,6 +40,7 @@
    17.4    System/download.scala
    17.5    System/event_bus.scala
    17.6    System/gui_setup.scala
    17.7 +  System/invoke_scala.scala
    17.8    System/isabelle_charset.scala
    17.9    System/isabelle_process.scala
   17.10    System/isabelle_syntax.scala
    18.1 --- a/src/Pure/library.scala	Mon Jul 11 07:04:30 2011 +0200
    18.2 +++ b/src/Pure/library.scala	Mon Jul 11 17:22:31 2011 +0200
    18.3 @@ -27,7 +27,7 @@
    18.4        exn match {
    18.5          case e: RuntimeException =>
    18.6            val msg = e.getMessage
    18.7 -          Some(if (msg == null) "" else msg)
    18.8 +          Some(if (msg == null) "Error" else msg)
    18.9          case _ => None
   18.10        }
   18.11    }