src/Pure/Concurrent/simple_thread.scala
author wenzelm
Mon, 23 Aug 2010 16:07:18 +0200
changeset 38636 b7647ca7de5a
child 38638 94ed0f34aea2
permissions -rw-r--r--
module for simplified thread operations (Scala version);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Concurrent/simple_thread.scala
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
     3
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
     4
Simplified thread operations.
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
     5
*/
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
     6
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
     7
package isabelle
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
     8
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
     9
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    10
import java.lang.Thread
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    11
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    12
import scala.actors.Actor
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    13
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    14
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    15
object Simple_Thread
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    16
{
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    17
  /* plain thread */
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    18
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    19
  def fork(name: String)(body: => Unit): Thread =
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    20
  {
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    21
    val thread = new Thread(name) { override def run = body }
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    22
    thread.start
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    23
    thread
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    24
  }
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    25
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    26
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    27
  /* thread as actor */
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    28
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    29
  def actor(name: String)(body: => Unit): Actor =
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    30
  {
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    31
    val actor = Future.promise[Actor]
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    32
    val thread = fork(name) { actor.fulfill(Actor.self); body }
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    33
    actor.join
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    34
  }
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    35
}
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    36