# HG changeset patch
# User wenzelm
# Date 1446565784 -3600
# Node ID f35786faee6cd781a564c1e93f0c5b16acaf7786
# Parent  7c985fd653c50effa65bc33f19fc138a8b5e18a5
prefer Isabelle/Scala Future;

diff -r 7c985fd653c5 -r f35786faee6c 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)
           })
diff -r 7c985fd653c5 -r f35786faee6c src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Nov 03 16:47:37 2015 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Nov 03 16:49:44 2015 +0100
@@ -10,7 +10,6 @@
 
 import isabelle._
 
-import java.util.concurrent.{Future => JFuture}
 import java.awt.{Color, Font, Toolkit, Window}
 import java.awt.event.KeyEvent
 import javax.swing.JTextField
@@ -75,7 +74,7 @@
   private var current_base_results = Command.Results.empty
   private var current_rendering: Rendering =
     Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
-  private var future_refresh: Option[JFuture[Unit]] = None
+  private var future_refresh: Option[Future[Unit]] = None
 
   private val rich_text_area =
     new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
@@ -128,9 +127,9 @@
       val base_results = current_base_results
       val formatted_body = Pretty.formatted(current_body, margin, metric)
 
-      future_refresh.map(_.cancel(true))
+      future_refresh.map(_.cancel)
       future_refresh =
-        Some(Standard_Thread.submit_task {
+        Some(Future.fork {
           val (text, rendering) =
             try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
             catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
diff -r 7c985fd653c5 -r f35786faee6c src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Tue Nov 03 16:47:37 2015 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Tue Nov 03 16:49:44 2015 +0100
@@ -11,7 +11,6 @@
 
 import scala.annotation.tailrec
 
-import java.util.concurrent.{Future => JFuture}
 import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension, Color}
 import java.awt.event.{MouseAdapter, MouseEvent}
 import javax.swing.{JPanel, ToolTipManager}
@@ -102,8 +101,8 @@
 
   /* asynchronous refresh */
 
-  private var future_refresh: Option[JFuture[Unit]] = None
-  private def cancel(): Unit = future_refresh.map(_.cancel(true))
+  private var future_refresh: Option[Future[Unit]] = None
+  private def cancel(): Unit = future_refresh.map(_.cancel)
 
   def invoke(): Unit = delay_refresh.invoke()
   def revoke(): Unit = delay_refresh.revoke()
@@ -128,7 +127,7 @@
             }
 
             future_refresh =
-              Some(Standard_Thread.submit_task {
+              Some(Future.fork {
                 val line_count = overview.line_count
                 val char_count = overview.char_count
                 val L = overview.L