equal
deleted
inserted
replaced
65 use "PIDE/xml.ML"; |
65 use "PIDE/xml.ML"; |
66 use "PIDE/yxml.ML"; |
66 use "PIDE/yxml.ML"; |
67 |
67 |
68 use "General/graph.ML"; |
68 use "General/graph.ML"; |
69 |
69 |
|
70 use "System/options.ML"; |
|
71 |
70 |
72 |
71 (* concurrency within the ML runtime *) |
73 (* concurrency within the ML runtime *) |
72 |
74 |
73 if ML_System.is_polyml |
75 if ML_System.is_polyml |
74 then use "ML/exn_properties_polyml.ML" |
76 then use "ML/exn_properties_polyml.ML" |
111 use "name.ML"; |
113 use "name.ML"; |
112 use "term.ML"; |
114 use "term.ML"; |
113 use "context.ML"; |
115 use "context.ML"; |
114 use "context_position.ML"; |
116 use "context_position.ML"; |
115 use "config.ML"; |
117 use "config.ML"; |
116 use "System/options.ML"; |
|
117 |
118 |
118 |
119 |
119 (* inner syntax *) |
120 (* inner syntax *) |
120 |
121 |
121 use "Syntax/term_position.ML"; |
122 use "Syntax/term_position.ML"; |