src/Pure/ROOT.ML
changeset 56287 ca090ae5f258
parent 56281 03c3d1a7c3b8
child 56288 bf1bdf335ea0
equal deleted inserted replaced
56286:7ede6ca96c61 56287:ca090ae5f258
    24 
    24 
    25 use "General/properties.ML";
    25 use "General/properties.ML";
    26 use "General/output.ML";
    26 use "General/output.ML";
    27 use "PIDE/markup.ML";
    27 use "PIDE/markup.ML";
    28 fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
    28 fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
    29 use "General/timing.ML";
       
    30 use "General/scan.ML";
    29 use "General/scan.ML";
    31 use "General/source.ML";
    30 use "General/source.ML";
    32 use "General/symbol.ML";
    31 use "General/symbol.ML";
    33 use "General/seq.ML";
       
    34 use "General/position.ML";
    32 use "General/position.ML";
    35 use "General/symbol_pos.ML";
    33 use "General/symbol_pos.ML";
    36 use "General/antiquote.ML";
    34 use "General/antiquote.ML";
    37 use "ML/ml_lex.ML";
    35 use "ML/ml_lex.ML";
    38 use "ML/ml_parse.ML";
    36 use "ML/ml_parse.ML";
    52 use "General/url.ML";
    50 use "General/url.ML";
    53 use "General/file.ML";
    51 use "General/file.ML";
    54 use "General/long_name.ML";
    52 use "General/long_name.ML";
    55 use "General/binding.ML";
    53 use "General/binding.ML";
    56 use "General/socket_io.ML";
    54 use "General/socket_io.ML";
       
    55 use "General/seq.ML";
       
    56 use "General/timing.ML";
    57 
    57 
    58 use "General/sha1.ML";
    58 use "General/sha1.ML";
    59 if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
    59 if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
    60 use "General/sha1_samples.ML";
    60 use "General/sha1_samples.ML";
    61 
    61