equal
deleted
inserted
replaced
75 |
75 |
76 if Multithreading.available |
76 if Multithreading.available |
77 then use "Concurrent/bash.ML" |
77 then use "Concurrent/bash.ML" |
78 else use "Concurrent/bash_sequential.ML"; |
78 else use "Concurrent/bash_sequential.ML"; |
79 |
79 |
80 use "Concurrent/mailbox.ML"; |
80 use "Concurrent/par_exn.ML"; |
81 use "Concurrent/task_queue.ML"; |
81 use "Concurrent/task_queue.ML"; |
82 use "Concurrent/future.ML"; |
82 use "Concurrent/future.ML"; |
83 |
83 |
84 use "Concurrent/lazy.ML"; |
84 use "Concurrent/lazy.ML"; |
85 if Multithreading.available then () |
85 if Multithreading.available then () |
87 |
87 |
88 use "Concurrent/par_list.ML"; |
88 use "Concurrent/par_list.ML"; |
89 if Multithreading.available then () |
89 if Multithreading.available then () |
90 else use "Concurrent/par_list_sequential.ML"; |
90 else use "Concurrent/par_list_sequential.ML"; |
91 |
91 |
|
92 use "Concurrent/mailbox.ML"; |
92 use "Concurrent/cache.ML"; |
93 use "Concurrent/cache.ML"; |
93 |
94 |
94 |
95 |
95 (* fundamental structures *) |
96 (* fundamental structures *) |
96 |
97 |