src/Pure/Concurrent/simple_thread.scala
author wenzelm
Thu, 24 Apr 2014 22:20:36 +0200
changeset 56707 aa4631879df8
parent 56704 c2f0ddd14747
child 56730 e723f041b6d0
permissions -rw-r--r--
obsolete;
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
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    14
object Simple_Thread
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    15
{
56667
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 49471
diff changeset
    16
  /* pending interrupts */
49471
97964515a676 text_rendering as managed task, with cancellation;
wenzelm
parents: 48355
diff changeset
    17
97964515a676 text_rendering as managed task, with cancellation;
wenzelm
parents: 48355
diff changeset
    18
  def interrupted_exception(): Unit =
56667
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 49471
diff changeset
    19
    if (Thread.interrupted()) throw Exn.Interrupt()
49471
97964515a676 text_rendering as managed task, with cancellation;
wenzelm
parents: 48355
diff changeset
    20
97964515a676 text_rendering as managed task, with cancellation;
wenzelm
parents: 48355
diff changeset
    21
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    22
  /* plain thread */
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    23
39577
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    24
  def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    25
  {
39577
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    26
    val thread =
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    27
      if (name == null || name == "") new Thread() { override def run = body }
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    28
      else new Thread(name) { override def run = body }
38638
94ed0f34aea2 optional daemon flag;
wenzelm
parents: 38636
diff changeset
    29
    thread.setDaemon(daemon)
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    30
    thread.start
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    31
    thread
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    32
  }
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    33
39579
wenzelm
parents: 39577
diff changeset
    34
wenzelm
parents: 39577
diff changeset
    35
  /* future result via thread */
39577
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    36
48355
6b36da29a0bf support for detached Bash_Job with some control operations;
wenzelm
parents: 45673
diff changeset
    37
  def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) =
39577
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    38
  {
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    39
    val result = Future.promise[A]
48355
6b36da29a0bf support for detached Bash_Job with some control operations;
wenzelm
parents: 45673
diff changeset
    40
    val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
6b36da29a0bf support for detached Bash_Job with some control operations;
wenzelm
parents: 45673
diff changeset
    41
    (thread, result)
39577
51bcd6003984 added Simple_Thread.future convenience;
wenzelm
parents: 39572
diff changeset
    42
  }
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    43
}
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents:
diff changeset
    44