| author | wenzelm |
| Sun, 16 Nov 2008 22:12:41 +0100 | |
| changeset 28815 | 80bb72a0f577 |
| parent 28574 | e73db43298a6 |
| child 29071 | 618216c658bb |
| permissions | -rw-r--r-- |
| 28308 | 1 |
(* Title: Pure/Concurrent/ROOT.ML |
| 28200 | 2 |
ID: $Id$ |
3 |
||
4 |
Concurrency within the ML runtime. |
|
5 |
*) |
|
6 |
||
|
28547
c81f6344bfb7
added future_scheduler flag (tmp!), from skip_proofs.ML;
wenzelm
parents:
28308
diff
changeset
|
7 |
val future_scheduler = ref false; |
|
c81f6344bfb7
added future_scheduler flag (tmp!), from skip_proofs.ML;
wenzelm
parents:
28308
diff
changeset
|
8 |
|
| 28240 | 9 |
use "simple_thread.ML"; |
| 28574 | 10 |
use "synchronized.ML"; |
| 28200 | 11 |
use "mailbox.ML"; |
12 |
use "schedule.ML"; |
|
13 |
use "task_queue.ML"; |
|
14 |
use "future.ML"; |
|
15 |
use "par_list.ML"; |
|
|
28547
c81f6344bfb7
added future_scheduler flag (tmp!), from skip_proofs.ML;
wenzelm
parents:
28308
diff
changeset
|
16 |
if Multithreading.available then () else use "par_list_dummy.ML"; |
|
c81f6344bfb7
added future_scheduler flag (tmp!), from skip_proofs.ML;
wenzelm
parents:
28308
diff
changeset
|
17 |