separate Concurrent/ROOT.ML;
authorwenzelm
Thu Sep 11 13:24:19 2008 +0200 (2008-09-11)
changeset 282005ef2c4bde4e5
parent 28199 e63d05ceec24
child 28201 7ae5cdb7b122
separate Concurrent/ROOT.ML;
src/Pure/Concurrent/ROOT.ML
src/Pure/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/ROOT.ML	Thu Sep 11 13:24:19 2008 +0200
     1.3 @@ -0,0 +1,11 @@
     1.4 +(*  Title:      Pure/General/ROOT.ML
     1.5 +    ID:         $Id$
     1.6 +
     1.7 +Concurrency within the ML runtime.
     1.8 +*)
     1.9 +
    1.10 +use "mailbox.ML";
    1.11 +use "schedule.ML";
    1.12 +use "task_queue.ML";
    1.13 +use "future.ML";
    1.14 +use "par_list.ML";
     2.1 --- a/src/Pure/ROOT.ML	Thu Sep 11 13:24:14 2008 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Thu Sep 11 13:24:19 2008 +0200
     2.3 @@ -21,12 +21,7 @@
     2.4  use "library.ML";
     2.5  
     2.6  cd "General"; use "ROOT.ML"; cd "..";
     2.7 -
     2.8 -(*concurrency within the ML runtime*)
     2.9 -use "Concurrent/mailbox.ML";
    2.10 -use "Concurrent/schedule.ML";
    2.11 -use "Concurrent/task_queue.ML";
    2.12 -use "Concurrent/future.ML";
    2.13 +cd "Concurrent"; use "ROOT.ML"; cd "..";
    2.14  
    2.15  (*fundamental structures*)
    2.16  use "name.ML";