src/Pure/Concurrent/ROOT.ML
author ballarin
Wed, 17 Dec 2008 17:53:41 +0100
changeset 29239 0a64c3418347
parent 29071 618216c658bb
child 29118 8f2481aa363d
permissions -rw-r--r--
Prevent defines from being checked in interpretation.
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
29071
618216c658bb enable future_scheduler by default;
wenzelm
parents: 28574
diff changeset
     7
val future_scheduler = ref true;
28547
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