src/Pure/ROOT.ML
changeset 44698 0385292321a0
parent 44549 5e5e6ad3922c
child 45026 5c0b0d67f9b1
equal deleted inserted replaced
44697:b99dfee76538 44698:0385292321a0
    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";