8 |
8 |
9 use "General/basics.ML"; |
9 use "General/basics.ML"; |
10 use "library.ML"; |
10 use "library.ML"; |
11 use "General/alist.ML"; |
11 use "General/alist.ML"; |
12 use "General/table.ML"; |
12 use "General/table.ML"; |
13 use "General/queue.ML"; |
|
14 use "General/graph.ML"; |
13 use "General/graph.ML"; |
|
14 |
|
15 structure Position = |
|
16 struct |
|
17 fun thread_data () = (); |
|
18 fun setmp_thread_data () f x = f x; |
|
19 end; |
|
20 |
|
21 structure Output = |
|
22 struct |
|
23 type output = string; |
|
24 fun escape s : output = s; |
|
25 fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); |
|
26 fun writeln s = raw_stdout (suffix "\n" s); |
|
27 fun warning s = writeln (prefix_lines "### " s); |
|
28 fun status (_: string) = (); |
|
29 end; |
|
30 val writeln = Output.writeln; |
|
31 val warning = Output.warning; |
|
32 fun print_mode_value () : string list = []; |
|
33 |
|
34 use "General/properties.ML"; |
|
35 use "General/timing.ML"; |
15 |
36 |
16 use "Concurrent/simple_thread.ML"; |
37 use "Concurrent/simple_thread.ML"; |
17 use "Concurrent/synchronized.ML"; |
38 use "Concurrent/synchronized.ML"; |
18 |
|
19 use "General/properties.ML"; |
|
20 use "General/print_mode.ML"; |
|
21 use "General/output.ML"; |
|
22 use "General/timing.ML"; |
|
23 use "General/markup.ML"; |
39 use "General/markup.ML"; |
24 use "General/scan.ML"; |
|
25 use "General/source.ML"; |
|
26 use "General/symbol.ML"; |
|
27 use "General/position.ML"; |
|
28 |
|
29 use "Concurrent/single_assignment.ML"; |
40 use "Concurrent/single_assignment.ML"; |
30 use "Concurrent/time_limit.ML"; |
41 use "Concurrent/time_limit.ML"; |
31 use "Concurrent/mailbox.ML"; |
|
32 use "Concurrent/task_queue.ML"; |
42 use "Concurrent/task_queue.ML"; |
33 use "Concurrent/future.ML"; |
43 use "Concurrent/future.ML"; |
34 use "Concurrent/lazy.ML"; |
44 use "Concurrent/lazy.ML"; |
35 use "Concurrent/par_list.ML"; |
45 use "Concurrent/par_list.ML"; |
|
46 |
|
47 use "General/queue.ML"; |
|
48 use "Concurrent/mailbox.ML"; |
36 use "Concurrent/cache.ML"; |
49 use "Concurrent/cache.ML"; |
37 |
50 |
38 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => |
51 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => |
39 pretty (Synchronized.value var, depth)); |
52 pretty (Synchronized.value var, depth)); |
40 |
53 |