# HG changeset patch # User wenzelm # Date 1313058250 -7200 # Node ID fdf0af3eaeb98c4529aee86e5ee4d80c4b5ccffe # Parent a34e6e2921151ba40e363fede14a6ad6d6dfaf3d some trimming; diff -r a34e6e292115 -r fdf0af3eaeb9 Admin/polyml/future/ROOT.ML --- a/Admin/polyml/future/ROOT.ML Thu Aug 11 12:11:50 2011 +0200 +++ b/Admin/polyml/future/ROOT.ML Thu Aug 11 12:24:10 2011 +0200 @@ -6,82 +6,32 @@ print_depth 10; - -(* library of general tools *) - use "General/basics.ML"; use "library.ML"; -use "General/print_mode.ML"; use "General/alist.ML"; use "General/table.ML"; +use "General/queue.ML"; +use "General/graph.ML"; use "Concurrent/simple_thread.ML"; - use "Concurrent/synchronized.ML"; -if Multithreading.available then () -else use "Concurrent/synchronized_sequential.ML"; use "General/properties.ML"; +use "General/print_mode.ML"; use "General/output.ML"; use "General/timing.ML"; use "General/markup.ML"; use "General/scan.ML"; use "General/source.ML"; use "General/symbol.ML"; -use "General/seq.ML"; use "General/position.ML"; -use "General/symbol_pos.ML"; -use "General/antiquote.ML"; -use "ML/ml_lex.ML"; -use "ML/ml_parse.ML"; -use "General/secure.ML"; -(*^^^^^ end of basic ML bootstrap ^^^^^*) -use "General/integer.ML"; -use "General/stack.ML"; -use "General/queue.ML"; -use "General/heap.ML"; -use "General/same.ML"; -use "General/ord_list.ML"; -use "General/balanced_tree.ML"; -use "General/graph.ML"; -use "General/linear_set.ML"; -use "General/buffer.ML"; -use "General/pretty.ML"; -use "General/xml.ML"; -use "General/path.ML"; -use "General/url.ML"; -use "General/file.ML"; -use "General/yxml.ML"; -use "General/long_name.ML"; -use "General/binding.ML"; - -use "General/sha1.ML"; -if ML_System.is_polyml then use "General/sha1_polyml.ML" else (); - - -(* concurrency within the ML runtime *) use "Concurrent/single_assignment.ML"; -if Multithreading.available then () -else use "Concurrent/single_assignment_sequential.ML"; - -if ML_System.is_smlnj then () else use "Concurrent/time_limit.ML"; - -if Multithreading.available -then use "Concurrent/bash.ML" -else use "Concurrent/bash_sequential.ML"; - +use "Concurrent/time_limit.ML"; use "Concurrent/mailbox.ML"; use "Concurrent/task_queue.ML"; use "Concurrent/future.ML"; - use "Concurrent/lazy.ML"; -if Multithreading.available then () -else use "Concurrent/lazy_sequential.ML"; - use "Concurrent/par_list.ML"; -if Multithreading.available then () -else use "Concurrent/par_list_sequential.ML"; - use "Concurrent/cache.ML";