tuned signature -- separate pool for JFuture tasks, which can be canceled;
authorwenzelm
Fri Apr 25 21:31:39 2014 +0200 (2014-04-25)
changeset 56730e723f041b6d0
parent 56729 1da2272a06a4
child 56731 326e8a7ea287
tuned signature -- separate pool for JFuture tasks, which can be canceled;
src/Pure/Concurrent/simple_thread.scala
src/Pure/System/invoke_scala.scala
src/Pure/library.scala
src/Tools/jEdit/src/pretty_text_area.scala
     1.1 --- a/src/Pure/Concurrent/simple_thread.scala	Fri Apr 25 20:21:27 2014 +0200
     1.2 +++ b/src/Pure/Concurrent/simple_thread.scala	Fri Apr 25 21:31:39 2014 +0200
     1.3 @@ -9,6 +9,9 @@
     1.4  
     1.5  
     1.6  import java.lang.Thread
     1.7 +import java.util.concurrent.{Callable, Future => JFuture}
     1.8 +
     1.9 +import scala.collection.parallel.ForkJoinTasks
    1.10  
    1.11  
    1.12  object Simple_Thread
    1.13 @@ -40,5 +43,13 @@
    1.14      val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
    1.15      (thread, result)
    1.16    }
    1.17 +
    1.18 +
    1.19 +  /* thread pool */
    1.20 +
    1.21 +  lazy val default_pool = ForkJoinTasks.defaultForkJoinPool
    1.22 +
    1.23 +  def submit_task[A](body: => A): JFuture[A] =
    1.24 +    default_pool.submit(new Callable[A] { def call = body })
    1.25  }
    1.26  
     2.1 --- a/src/Pure/System/invoke_scala.scala	Fri Apr 25 20:21:27 2014 +0200
     2.2 +++ b/src/Pure/System/invoke_scala.scala	Fri Apr 25 21:31:39 2014 +0200
     2.3 @@ -8,6 +8,8 @@
     2.4  
     2.5  
     2.6  import java.lang.reflect.{Method, Modifier, InvocationTargetException}
     2.7 +import java.util.concurrent.{Future => JFuture}
     2.8 +
     2.9  import scala.util.matching.Regex
    2.10  
    2.11  
    2.12 @@ -70,7 +72,7 @@
    2.13  
    2.14  class Invoke_Scala extends Session.Protocol_Handler
    2.15  {
    2.16 -  private var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
    2.17 +  private var futures = Map.empty[String, JFuture[Unit]]
    2.18  
    2.19    private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
    2.20      synchronized
    2.21 @@ -81,7 +83,7 @@
    2.22        }
    2.23      }
    2.24  
    2.25 -  private def cancel(prover: Prover, id: String, future: java.util.concurrent.Future[Unit])
    2.26 +  private def cancel(prover: Prover, id: String, future: JFuture[Unit])
    2.27    {
    2.28      future.cancel(true)
    2.29      fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
    2.30 @@ -92,11 +94,10 @@
    2.31      msg.properties match {
    2.32        case Markup.Invoke_Scala(name, id) =>
    2.33          futures += (id ->
    2.34 -          default_thread_pool.submit(() =>
    2.35 -            {
    2.36 -              val (tag, result) = Invoke_Scala.method(name, msg.text)
    2.37 -              fulfill(prover, id, tag, result)
    2.38 -            }))
    2.39 +          Simple_Thread.submit_task {
    2.40 +            val (tag, result) = Invoke_Scala.method(name, msg.text)
    2.41 +            fulfill(prover, id, tag, result)
    2.42 +          })
    2.43          true
    2.44        case _ => false
    2.45      }
     3.1 --- a/src/Pure/library.scala	Fri Apr 25 20:21:27 2014 +0200
     3.2 +++ b/src/Pure/library.scala	Fri Apr 25 21:31:39 2014 +0200
     3.3 @@ -10,8 +10,6 @@
     3.4  
     3.5  import scala.collection.mutable
     3.6  
     3.7 -import java.util.concurrent.{Future => JFuture, TimeUnit}
     3.8 -
     3.9  
    3.10  object Library
    3.11  {
    3.12 @@ -174,13 +172,4 @@
    3.13    val quote = Library.quote _
    3.14    val commas = Library.commas _
    3.15    val commas_quote = Library.commas_quote _
    3.16 -
    3.17 -
    3.18 -  /* parallel tasks */
    3.19 -
    3.20 -  implicit def function_as_callable[A](f: () => A) =
    3.21 -    new java.util.concurrent.Callable[A] { def call = f() }
    3.22 -
    3.23 -  val default_thread_pool =
    3.24 -    scala.collection.parallel.ForkJoinTasks.defaultForkJoinPool
    3.25  }
     4.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Apr 25 20:21:27 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Apr 25 21:31:39 2014 +0200
     4.3 @@ -12,6 +12,7 @@
     4.4  
     4.5  import java.awt.{Color, Font, FontMetrics, Toolkit, Window}
     4.6  import java.awt.event.KeyEvent
     4.7 +import java.util.concurrent.{Future => JFuture}
     4.8  
     4.9  import org.gjt.sp.jedit.{jEdit, View, Registers}
    4.10  import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
    4.11 @@ -67,7 +68,7 @@
    4.12    private var current_base_results = Command.Results.empty
    4.13    private var current_rendering: Rendering =
    4.14      Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
    4.15 -  private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
    4.16 +  private var future_rendering: Option[JFuture[Unit]] = None
    4.17  
    4.18    private val rich_text_area =
    4.19      new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
    4.20 @@ -118,8 +119,8 @@
    4.21        val formatted_body = Pretty.formatted(current_body, margin, metric)
    4.22  
    4.23        future_rendering.map(_.cancel(true))
    4.24 -      future_rendering = Some(default_thread_pool.submit(() =>
    4.25 -        {
    4.26 +      future_rendering =
    4.27 +        Some(Simple_Thread.submit_task {
    4.28            val (text, rendering) =
    4.29              try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
    4.30              catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
    4.31 @@ -136,7 +137,7 @@
    4.32                getBuffer.setReadOnly(true)
    4.33              }
    4.34            }
    4.35 -        }))
    4.36 +        })
    4.37      }
    4.38    }
    4.39