src/Pure/Concurrent/ROOT.ML
author wenzelm
Wed, 10 Dec 2008 22:05:58 +0100
changeset 29055 edaef19665e6
parent 28574 e73db43298a6
child 29071 618216c658bb
permissions -rw-r--r--
merged
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28308
d4396a28fb29 fixed headers
haftmann
parents: 28240
diff changeset
     1
(*  Title:      Pure/Concurrent/ROOT.ML
28200
5ef2c4bde4e5 separate Concurrent/ROOT.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
5ef2c4bde4e5 separate Concurrent/ROOT.ML;
wenzelm
parents:
diff changeset
     3
5ef2c4bde4e5 separate Concurrent/ROOT.ML;
wenzelm
parents:
diff changeset
     4
Concurrency within the ML runtime.
5ef2c4bde4e5 separate Concurrent/ROOT.ML;
wenzelm
parents:
diff changeset
     5
*)
5ef2c4bde4e5 separate Concurrent/ROOT.ML;
wenzelm
parents:
diff changeset
     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
444d1e8ae496 added Concurrent/simple_thread.ML;
wenzelm
parents: 28200
diff changeset
     9
use "simple_thread.ML";
28574
e73db43298a6 added Concurrent/synchronized.ML;
wenzelm
parents: 28547
diff changeset
    10
use "synchronized.ML";
28200
5ef2c4bde4e5 separate Concurrent/ROOT.ML;
wenzelm
parents:
diff changeset
    11
use "mailbox.ML";
5ef2c4bde4e5 separate Concurrent/ROOT.ML;
wenzelm
parents:
diff changeset
    12
use "schedule.ML";
5ef2c4bde4e5 separate Concurrent/ROOT.ML;
wenzelm
parents:
diff changeset
    13
use "task_queue.ML";
5ef2c4bde4e5 separate Concurrent/ROOT.ML;
wenzelm
parents:
diff changeset
    14
use "future.ML";
5ef2c4bde4e5 separate Concurrent/ROOT.ML;
wenzelm
parents:
diff changeset
    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