src/Pure/Concurrent/simple_thread.scala
author wenzelm
Tue, 29 Nov 2011 21:29:53 +0100
changeset 45673 cd41e3903fbf
parent 45667 546d78f0d81f
child 48355 6b36da29a0bf
permissions -rw-r--r--
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
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
45673
cd41e3903fbf separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents: 45667
diff changeset
     2
    Module:     PIDE
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
     4
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
     5
Simplified thread operations.
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
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
     8
package isabelle
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
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    11
import java.lang.Thread
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    12
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    13
import scala.actors.Actor
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
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    16
object Simple_Thread
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    17
{
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    18
  /* plain thread */
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    19
39577
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    20
  def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    21
  {
39577
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    22
    val thread =
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    23
      if (name == null || name == "") new Thread() { override def run = body }
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    24
      else new Thread(name) { override def run = body }
38638
94ed0f34aea2 optional daemon flag;
wenzelm
parents: 38636
diff changeset
    25
    thread.setDaemon(daemon)
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    26
    thread.start
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    27
    thread
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
39579
wenzelm
parents: 39577
diff changeset
    30
wenzelm
parents: 39577
diff changeset
    31
  /* future result via thread */
39577
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    32
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    33
  def future[A](name: String = "", daemon: Boolean = false)(body: => A): Future[A] =
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    34
  {
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    35
    val result = Future.promise[A]
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    36
    fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    37
    result
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    38
  }
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    39
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    40
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    41
  /* thread as actor */
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    42
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 38638
diff changeset
    43
  def actor(name: String, daemon: Boolean = false)(body: => Unit): (Thread, Actor) =
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    44
  {
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    45
    val actor = Future.promise[Actor]
38638
94ed0f34aea2 optional daemon flag;
wenzelm
parents: 38636
diff changeset
    46
    val thread = fork(name, daemon) { actor.fulfill(Actor.self); body }
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 38638
diff changeset
    47
    (thread, actor.join)
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    48
  }
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    49
}
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    50