src/Pure/General/ROOT.ML
changeset 12420 a2a05c952b4d
parent 9119 8ca79837b41b
child 14278 ae499452700a
equal deleted inserted replaced
12419:6a7ee57447aa 12420:a2a05c952b4d
    18 use "url.ML";
    18 use "url.ML";
    19 use "file.ML";
    19 use "file.ML";
    20 use "buffer.ML";
    20 use "buffer.ML";
    21 use "history.ML";
    21 use "history.ML";
    22 use "pretty.ML";
    22 use "pretty.ML";
       
    23 use "xml.ML";
    23 
    24 
    24 structure PureGeneral =
    25 structure PureGeneral =
    25 struct
    26 struct
    26   structure Symtab = Symtab;
    27   structure Symtab = Symtab;
    27   structure Graph = Graph;
    28   structure Graph = Graph;
    36   structure Url = Url;
    37   structure Url = Url;
    37   structure File = File;
    38   structure File = File;
    38   structure Buffer = Buffer;
    39   structure Buffer = Buffer;
    39   structure History = History;
    40   structure History = History;
    40   structure Pretty = Pretty;
    41   structure Pretty = Pretty;
       
    42   structure XML = XML;
    41 end;
    43 end;