equal
deleted
inserted
replaced
52 use "General/balanced_tree.ML"; |
52 use "General/balanced_tree.ML"; |
53 use "General/graph.ML"; |
53 use "General/graph.ML"; |
54 use "General/linear_set.ML"; |
54 use "General/linear_set.ML"; |
55 use "General/buffer.ML"; |
55 use "General/buffer.ML"; |
56 use "General/pretty.ML"; |
56 use "General/pretty.ML"; |
57 use "General/xml.ML"; |
|
58 use "General/path.ML"; |
57 use "General/path.ML"; |
59 use "General/url.ML"; |
58 use "General/url.ML"; |
60 use "General/file.ML"; |
59 use "General/file.ML"; |
61 use "General/yxml.ML"; |
|
62 use "General/long_name.ML"; |
60 use "General/long_name.ML"; |
63 use "General/binding.ML"; |
61 use "General/binding.ML"; |
64 |
62 |
65 use "General/sha1.ML"; |
63 use "General/sha1.ML"; |
66 if ML_System.is_polyml then use "General/sha1_polyml.ML" else (); |
64 if ML_System.is_polyml then use "General/sha1_polyml.ML" else (); |
|
65 |
|
66 use "PIDE/xml.ML"; |
|
67 use "PIDE/yxml.ML"; |
67 |
68 |
68 |
69 |
69 (* concurrency within the ML runtime *) |
70 (* concurrency within the ML runtime *) |
70 |
71 |
71 use "Concurrent/single_assignment.ML"; |
72 use "Concurrent/single_assignment.ML"; |