diff -r 3d37b2957a3e -r c39972ddd672 src/Pure/System/invoke_scala.scala
--- a/src/Pure/System/invoke_scala.scala	Thu Nov 14 17:39:32 2013 +0100
+++ b/src/Pure/System/invoke_scala.scala	Fri Nov 15 19:31:10 2013 +0100
@@ -89,15 +89,14 @@
   }
 
   private def invoke_scala(
-    prover: Session.Prover, output: Isabelle_Process.Output): Boolean = synchronized
+    prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = synchronized
   {
-    output.properties match {
+    msg.properties match {
       case Markup.Invoke_Scala(name, id) =>
         futures += (id ->
           default_thread_pool.submit(() =>
             {
-              val arg = XML.content(output.body)
-              val (tag, result) = Invoke_Scala.method(name, arg)
+              val (tag, result) = Invoke_Scala.method(name, msg.text)
               fulfill(prover, id, tag, result)
             }))
         true
@@ -106,9 +105,9 @@
   }
 
   private def cancel_scala(
-    prover: Session.Prover, output: Isabelle_Process.Output): Boolean = synchronized
+    prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = synchronized
   {
-    output.properties match {
+    msg.properties match {
       case Markup.Cancel_Scala(id) =>
         futures.get(id) match {
           case Some(future) => cancel(prover, id, future)