src/Pure/ROOT.ML
changeset 32840 75dff0bd4d5d
parent 32816 5db89f8d44f3
child 33374 8099185908a4
     1.1 --- a/src/Pure/ROOT.ML	Thu Oct 01 20:47:26 2009 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Thu Oct 01 22:39:06 2009 +0200
     1.3 @@ -56,19 +56,25 @@
     1.4  (* concurrency within the ML runtime *)
     1.5  
     1.6  use "Concurrent/simple_thread.ML";
     1.7 +
     1.8  use "Concurrent/synchronized.ML";
     1.9  if Multithreading.available then ()
    1.10  else use "Concurrent/synchronized_sequential.ML";
    1.11 +
    1.12  use "Concurrent/mailbox.ML";
    1.13  use "Concurrent/task_queue.ML";
    1.14  use "Concurrent/future.ML";
    1.15 +
    1.16  use "Concurrent/lazy.ML";
    1.17  if Multithreading.available then ()
    1.18  else use "Concurrent/lazy_sequential.ML";
    1.19 +
    1.20  use "Concurrent/par_list.ML";
    1.21  if Multithreading.available then ()
    1.22  else use "Concurrent/par_list_sequential.ML";
    1.23  
    1.24 +use "Concurrent/cache.ML";
    1.25 +
    1.26  
    1.27  (* fundamental structures *)
    1.28