equal
deleted
inserted
replaced
26 if Multithreading.available then () |
26 if Multithreading.available then () |
27 else use "Concurrent/synchronized_sequential.ML"; |
27 else use "Concurrent/synchronized_sequential.ML"; |
28 |
28 |
29 use "General/properties.ML"; |
29 use "General/properties.ML"; |
30 use "General/output.ML"; |
30 use "General/output.ML"; |
31 use "General/timing.ML"; |
|
32 use "PIDE/markup.ML"; |
31 use "PIDE/markup.ML"; |
33 fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s)); |
32 fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s)); |
|
33 use "General/timing.ML"; |
34 use "General/scan.ML"; |
34 use "General/scan.ML"; |
35 use "General/source.ML"; |
35 use "General/source.ML"; |
36 use "General/symbol.ML"; |
36 use "General/symbol.ML"; |
37 use "General/seq.ML"; |
37 use "General/seq.ML"; |
38 use "General/position.ML"; |
38 use "General/position.ML"; |