module for simplified thread operations (Scala version);
authorwenzelm
Mon Aug 23 16:07:18 2010 +0200 (2010-08-23)
changeset 38636b7647ca7de5a
parent 38635 f76ad0771f67
child 38637 03b27bd0505e
module for simplified thread operations (Scala version);
src/Pure/Concurrent/simple_thread.scala
src/Pure/System/isabelle_process.scala
src/Pure/build-jars
src/Pure/library.scala
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/simple_thread.scala	Mon Aug 23 16:07:18 2010 +0200
     1.3 @@ -0,0 +1,36 @@
     1.4 +/*  Title:      Pure/Concurrent/simple_thread.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Simplified thread operations.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import java.lang.Thread
    1.14 +
    1.15 +import scala.actors.Actor
    1.16 +
    1.17 +
    1.18 +object Simple_Thread
    1.19 +{
    1.20 +  /* plain thread */
    1.21 +
    1.22 +  def fork(name: String)(body: => Unit): Thread =
    1.23 +  {
    1.24 +    val thread = new Thread(name) { override def run = body }
    1.25 +    thread.start
    1.26 +    thread
    1.27 +  }
    1.28 +
    1.29 +
    1.30 +  /* thread as actor */
    1.31 +
    1.32 +  def actor(name: String)(body: => Unit): Actor =
    1.33 +  {
    1.34 +    val actor = Future.promise[Actor]
    1.35 +    val thread = fork(name) { actor.fulfill(Actor.self); body }
    1.36 +    actor.join
    1.37 +  }
    1.38 +}
    1.39 +
     2.1 --- a/src/Pure/System/isabelle_process.scala	Mon Aug 23 15:11:41 2010 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Aug 23 16:07:18 2010 +0200
     2.3 @@ -155,7 +155,7 @@
     2.4    /* raw stdin */
     2.5  
     2.6    private def stdin_actor(name: String, stream: OutputStream): Actor =
     2.7 -    Library.thread_actor(name) {
     2.8 +    Simple_Thread.actor(name) {
     2.9        val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset))
    2.10        var finished = false
    2.11        while (!finished) {
    2.12 @@ -184,7 +184,7 @@
    2.13    /* raw stdout */
    2.14  
    2.15    private def stdout_actor(name: String, stream: InputStream): Actor =
    2.16 -    Library.thread_actor(name) {
    2.17 +    Simple_Thread.actor(name) {
    2.18        val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
    2.19        var result = new StringBuilder(100)
    2.20  
    2.21 @@ -221,7 +221,7 @@
    2.22    /* command input */
    2.23  
    2.24    private def input_actor(name: String, raw_stream: OutputStream): Actor =
    2.25 -    Library.thread_actor(name) {
    2.26 +    Simple_Thread.actor(name) {
    2.27        val stream = new BufferedOutputStream(raw_stream)
    2.28        var finished = false
    2.29        while (!finished) {
    2.30 @@ -253,7 +253,7 @@
    2.31    private class Protocol_Error(msg: String) extends Exception(msg)
    2.32  
    2.33    private def message_actor(name: String, stream: InputStream): Actor =
    2.34 -    Library.thread_actor(name) {
    2.35 +    Simple_Thread.actor(name) {
    2.36        val default_buffer = new Array[Byte](65536)
    2.37        var c = -1
    2.38  
    2.39 @@ -344,7 +344,7 @@
    2.40  
    2.41    /* exit process */
    2.42  
    2.43 -  Library.thread_actor("process_exit") {
    2.44 +  Simple_Thread.actor("process_exit") {
    2.45      proc match {
    2.46        case None =>
    2.47        case Some(p) =>
     3.1 --- a/src/Pure/build-jars	Mon Aug 23 15:11:41 2010 +0200
     3.2 +++ b/src/Pure/build-jars	Mon Aug 23 16:07:18 2010 +0200
     3.3 @@ -23,6 +23,7 @@
     3.4  
     3.5  declare -a SOURCES=(
     3.6    Concurrent/future.scala
     3.7 +  Concurrent/simple_thread.scala
     3.8    General/exn.scala
     3.9    General/linear_set.scala
    3.10    General/markup.scala
     4.1 --- a/src/Pure/library.scala	Mon Aug 23 15:11:41 2010 +0200
     4.2 +++ b/src/Pure/library.scala	Mon Aug 23 16:07:18 2010 +0200
     4.3 @@ -7,11 +7,10 @@
     4.4  package isabelle
     4.5  
     4.6  
     4.7 -import java.lang.{System, Thread}
     4.8 +import java.lang.System
     4.9  import java.awt.Component
    4.10  import javax.swing.JOptionPane
    4.11  
    4.12 -import scala.actors.Actor
    4.13  import scala.swing.ComboBox
    4.14  import scala.swing.event.SelectionChanged
    4.15  
    4.16 @@ -139,15 +138,4 @@
    4.17          ((stop - start).toDouble / 1000000) + "ms elapsed time")
    4.18      Exn.release(result)
    4.19    }
    4.20 -
    4.21 -
    4.22 -  /* thread as actor */
    4.23 -
    4.24 -  def thread_actor(name: String)(body: => Unit): Actor =
    4.25 -  {
    4.26 -    val actor = Future.promise[Actor]
    4.27 -    val thread = new Thread(name) { override def run() = { actor.fulfill(Actor.self); body } }
    4.28 -    thread.start
    4.29 -    actor.join
    4.30 -  }
    4.31  }