4 |
4 |
5 use "ML-Systems/polyml.ML"; |
5 use "ML-Systems/polyml.ML"; |
6 |
6 |
7 print_depth 10; |
7 print_depth 10; |
8 |
8 |
9 |
|
10 (* library of general tools *) |
|
11 |
|
12 use "General/basics.ML"; |
9 use "General/basics.ML"; |
13 use "library.ML"; |
10 use "library.ML"; |
14 use "General/print_mode.ML"; |
|
15 use "General/alist.ML"; |
11 use "General/alist.ML"; |
16 use "General/table.ML"; |
12 use "General/table.ML"; |
|
13 use "General/queue.ML"; |
|
14 use "General/graph.ML"; |
17 |
15 |
18 use "Concurrent/simple_thread.ML"; |
16 use "Concurrent/simple_thread.ML"; |
19 |
|
20 use "Concurrent/synchronized.ML"; |
17 use "Concurrent/synchronized.ML"; |
21 if Multithreading.available then () |
|
22 else use "Concurrent/synchronized_sequential.ML"; |
|
23 |
18 |
24 use "General/properties.ML"; |
19 use "General/properties.ML"; |
|
20 use "General/print_mode.ML"; |
25 use "General/output.ML"; |
21 use "General/output.ML"; |
26 use "General/timing.ML"; |
22 use "General/timing.ML"; |
27 use "General/markup.ML"; |
23 use "General/markup.ML"; |
28 use "General/scan.ML"; |
24 use "General/scan.ML"; |
29 use "General/source.ML"; |
25 use "General/source.ML"; |
30 use "General/symbol.ML"; |
26 use "General/symbol.ML"; |
31 use "General/seq.ML"; |
|
32 use "General/position.ML"; |
27 use "General/position.ML"; |
33 use "General/symbol_pos.ML"; |
|
34 use "General/antiquote.ML"; |
|
35 use "ML/ml_lex.ML"; |
|
36 use "ML/ml_parse.ML"; |
|
37 use "General/secure.ML"; |
|
38 (*^^^^^ end of basic ML bootstrap ^^^^^*) |
|
39 use "General/integer.ML"; |
|
40 use "General/stack.ML"; |
|
41 use "General/queue.ML"; |
|
42 use "General/heap.ML"; |
|
43 use "General/same.ML"; |
|
44 use "General/ord_list.ML"; |
|
45 use "General/balanced_tree.ML"; |
|
46 use "General/graph.ML"; |
|
47 use "General/linear_set.ML"; |
|
48 use "General/buffer.ML"; |
|
49 use "General/pretty.ML"; |
|
50 use "General/xml.ML"; |
|
51 use "General/path.ML"; |
|
52 use "General/url.ML"; |
|
53 use "General/file.ML"; |
|
54 use "General/yxml.ML"; |
|
55 use "General/long_name.ML"; |
|
56 use "General/binding.ML"; |
|
57 |
|
58 use "General/sha1.ML"; |
|
59 if ML_System.is_polyml then use "General/sha1_polyml.ML" else (); |
|
60 |
|
61 |
|
62 (* concurrency within the ML runtime *) |
|
63 |
28 |
64 use "Concurrent/single_assignment.ML"; |
29 use "Concurrent/single_assignment.ML"; |
65 if Multithreading.available then () |
30 use "Concurrent/time_limit.ML"; |
66 else use "Concurrent/single_assignment_sequential.ML"; |
|
67 |
|
68 if ML_System.is_smlnj then () else use "Concurrent/time_limit.ML"; |
|
69 |
|
70 if Multithreading.available |
|
71 then use "Concurrent/bash.ML" |
|
72 else use "Concurrent/bash_sequential.ML"; |
|
73 |
|
74 use "Concurrent/mailbox.ML"; |
31 use "Concurrent/mailbox.ML"; |
75 use "Concurrent/task_queue.ML"; |
32 use "Concurrent/task_queue.ML"; |
76 use "Concurrent/future.ML"; |
33 use "Concurrent/future.ML"; |
77 |
|
78 use "Concurrent/lazy.ML"; |
34 use "Concurrent/lazy.ML"; |
79 if Multithreading.available then () |
|
80 else use "Concurrent/lazy_sequential.ML"; |
|
81 |
|
82 use "Concurrent/par_list.ML"; |
35 use "Concurrent/par_list.ML"; |
83 if Multithreading.available then () |
|
84 else use "Concurrent/par_list_sequential.ML"; |
|
85 |
|
86 use "Concurrent/cache.ML"; |
36 use "Concurrent/cache.ML"; |
87 |
37 |