src/Pure/ROOT.ML
changeset 51606 2843cc095a57
parent 51551 88d1d19fb74f
child 51933 a60c6c90a447
equal deleted inserted replaced
51605:eca8acb42e4a 51606:2843cc095a57
    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";