src/Pure/System/invoke_scala.scala

--- a/src/Pure/System/invoke_scala.scala	Tue Nov 03 16:47:37 2015 +0100
+++ b/src/Pure/System/invoke_scala.scala	Tue Nov 03 16:49:44 2015 +0100
@@ -8,7 +8,6 @@
 
 
 import java.lang.reflect.{Method, Modifier, InvocationTargetException}
-import java.util.concurrent.{Future => JFuture}
 
 import scala.util.matching.Regex
 
@@ -72,7 +71,7 @@
 
 class Invoke_Scala extends Session.Protocol_Handler
 {
-  private var futures = Map.empty[String, JFuture[Unit]]
+  private var futures = Map.empty[String, Future[Unit]]
 
   private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
     synchronized
@@ -83,9 +82,9 @@
       }
     }
 
-  private def cancel(prover: Prover, id: String, future: JFuture[Unit])
+  private def cancel(prover: Prover, id: String, future: Future[Unit])
   {
-    future.cancel(true)
+    future.cancel
     fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
   }
 
@@ -94,7 +93,7 @@
     msg.properties match {
       case Markup.Invoke_Scala(name, id) =>
         futures += (id ->
-          Standard_Thread.submit_task {
+          Future.fork {
             val (tag, result) = Invoke_Scala.method(name, msg.text)
             fulfill(prover, id, tag, result)
           })