| author | wenzelm | 
| Thu, 24 Apr 2014 22:20:36 +0200 | |
| changeset 56707 | aa4631879df8 | 
| parent 56704 | c2f0ddd14747 | 
| child 56730 | e723f041b6d0 | 
| permissions | -rw-r--r-- | 
| 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: 
45667diff
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: 
49471diff
changeset | 16 | /* pending interrupts */ | 
| 49471 
97964515a676
text_rendering as managed task, with cancellation;
 wenzelm parents: 
48355diff
changeset | 17 | |
| 
97964515a676
text_rendering as managed task, with cancellation;
 wenzelm parents: 
48355diff
changeset | 18 | def interrupted_exception(): Unit = | 
| 56667 
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
 wenzelm parents: 
49471diff
changeset | 19 | if (Thread.interrupted()) throw Exn.Interrupt() | 
| 49471 
97964515a676
text_rendering as managed task, with cancellation;
 wenzelm parents: 
48355diff
changeset | 20 | |
| 
97964515a676
text_rendering as managed task, with cancellation;
 wenzelm parents: 
48355diff
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 | 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 | 26 | val thread = | 
| 27 |       if (name == null || name == "") new Thread() { override def run = body }
 | |
| 28 |       else new Thread(name) { override def run = body }
 | |
| 38638 | 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 | 34 | |
| 35 | /* future result via thread */ | |
| 39577 | 36 | |
| 48355 
6b36da29a0bf
support for detached Bash_Job with some control operations;
 wenzelm parents: 
45673diff
changeset | 37 | def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) = | 
| 39577 | 38 |   {
 | 
| 39 | val result = Future.promise[A] | |
| 48355 
6b36da29a0bf
support for detached Bash_Job with some control operations;
 wenzelm parents: 
45673diff
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: 
45673diff
changeset | 41 | (thread, result) | 
| 39577 | 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 |