# HG changeset patch
# User wenzelm
# Date 1398454299 -7200
# Node ID e723f041b6d0088d16559abc79da8a443cc559a0
# Parent  1da2272a06a451a3cb20414056cc6e921703ea0a
tuned signature -- separate pool for JFuture tasks, which can be canceled;

diff -r 1da2272a06a4 -r e723f041b6d0 src/Pure/Concurrent/simple_thread.scala
--- a/src/Pure/Concurrent/simple_thread.scala	Fri Apr 25 20:21:27 2014 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala	Fri Apr 25 21:31:39 2014 +0200
@@ -9,6 +9,9 @@
 
 
 import java.lang.Thread
+import java.util.concurrent.{Callable, Future => JFuture}
+
+import scala.collection.parallel.ForkJoinTasks
 
 
 object Simple_Thread
@@ -40,5 +43,13 @@
     val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
     (thread, result)
   }
+
+
+  /* thread pool */
+
+  lazy val default_pool = ForkJoinTasks.defaultForkJoinPool
+
+  def submit_task[A](body: => A): JFuture[A] =
+    default_pool.submit(new Callable[A] { def call = body })
 }
 
diff -r 1da2272a06a4 -r e723f041b6d0 src/Pure/System/invoke_scala.scala
--- a/src/Pure/System/invoke_scala.scala	Fri Apr 25 20:21:27 2014 +0200
+++ b/src/Pure/System/invoke_scala.scala	Fri Apr 25 21:31:39 2014 +0200
@@ -8,6 +8,8 @@
 
 
 import java.lang.reflect.{Method, Modifier, InvocationTargetException}
+import java.util.concurrent.{Future => JFuture}
+
 import scala.util.matching.Regex
 
 
@@ -70,7 +72,7 @@
 
 class Invoke_Scala extends Session.Protocol_Handler
 {
-  private var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
+  private var futures = Map.empty[String, JFuture[Unit]]
 
   private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
     synchronized
@@ -81,7 +83,7 @@
       }
     }
 
-  private def cancel(prover: Prover, id: String, future: java.util.concurrent.Future[Unit])
+  private def cancel(prover: Prover, id: String, future: JFuture[Unit])
   {
     future.cancel(true)
     fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
@@ -92,11 +94,10 @@
     msg.properties match {
       case Markup.Invoke_Scala(name, id) =>
         futures += (id ->
-          default_thread_pool.submit(() =>
-            {
-              val (tag, result) = Invoke_Scala.method(name, msg.text)
-              fulfill(prover, id, tag, result)
-            }))
+          Simple_Thread.submit_task {
+            val (tag, result) = Invoke_Scala.method(name, msg.text)
+            fulfill(prover, id, tag, result)
+          })
         true
       case _ => false
     }
diff -r 1da2272a06a4 -r e723f041b6d0 src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Apr 25 20:21:27 2014 +0200
+++ b/src/Pure/library.scala	Fri Apr 25 21:31:39 2014 +0200
@@ -10,8 +10,6 @@
 
 import scala.collection.mutable
 
-import java.util.concurrent.{Future => JFuture, TimeUnit}
-
 
 object Library
 {
@@ -174,13 +172,4 @@
   val quote = Library.quote _
   val commas = Library.commas _
   val commas_quote = Library.commas_quote _
-
-
-  /* parallel tasks */
-
-  implicit def function_as_callable[A](f: () => A) =
-    new java.util.concurrent.Callable[A] { def call = f() }
-
-  val default_thread_pool =
-    scala.collection.parallel.ForkJoinTasks.defaultForkJoinPool
 }
diff -r 1da2272a06a4 -r e723f041b6d0 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Apr 25 20:21:27 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Apr 25 21:31:39 2014 +0200
@@ -12,6 +12,7 @@
 
 import java.awt.{Color, Font, FontMetrics, Toolkit, Window}
 import java.awt.event.KeyEvent
+import java.util.concurrent.{Future => JFuture}
 
 import org.gjt.sp.jedit.{jEdit, View, Registers}
 import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
@@ -67,7 +68,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_rendering: Option[java.util.concurrent.Future[Unit]] = None
+  private var future_rendering: Option[JFuture[Unit]] = None
 
   private val rich_text_area =
     new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
@@ -118,8 +119,8 @@
       val formatted_body = Pretty.formatted(current_body, margin, metric)
 
       future_rendering.map(_.cancel(true))
-      future_rendering = Some(default_thread_pool.submit(() =>
-        {
+      future_rendering =
+        Some(Simple_Thread.submit_task {
           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 }
@@ -136,7 +137,7 @@
               getBuffer.setReadOnly(true)
             }
           }
-        }))
+        })
     }
   }