src/Pure/General/ROOT.ML
changeset 6634 6f74e7aa5b4d
parent 6317 128e592f5489
child 6638 731b4aec2fd6
equal deleted inserted replaced
6633:2ed30ebd7e31 6634:6f74e7aa5b4d
     8 use "graph.ML";
     8 use "graph.ML";
     9 use "object.ML";
     9 use "object.ML";
    10 use "seq.ML";
    10 use "seq.ML";
    11 use "name_space.ML";
    11 use "name_space.ML";
    12 use "position.ML";
    12 use "position.ML";
       
    13 use "scan.ML";
    13 use "path.ML";
    14 use "path.ML";
    14 use "file.ML";
    15 use "file.ML";
    15 use "buffer.ML";
    16 use "buffer.ML";
    16 use "history.ML";
    17 use "history.ML";
    17 use "scan.ML";
       
    18 use "source.ML";
    18 use "source.ML";
    19 use "symbol.ML";
    19 use "symbol.ML";
    20 use "pretty.ML";
    20 use "pretty.ML";
    21 
    21 
    22 structure PureGeneral =
    22 structure PureGeneral =
    25   structure Graph = Graph;
    25   structure Graph = Graph;
    26   structure Object = Object;
    26   structure Object = Object;
    27   structure Seq = Seq;
    27   structure Seq = Seq;
    28   structure NameSpace = NameSpace;
    28   structure NameSpace = NameSpace;
    29   structure Position = Position;
    29   structure Position = Position;
       
    30   structure Scan = Scan;
    30   structure Path = Path;
    31   structure Path = Path;
    31   structure File = File;
    32   structure File = File;
    32   structure Buffer = Buffer;
    33   structure Buffer = Buffer;
    33   structure History = History;
    34   structure History = History;
    34   structure Scan = Scan;
       
    35   structure Source = Source;
    35   structure Source = Source;
    36   structure Symbol = Symbol;
    36   structure Symbol = Symbol;
    37   structure Pretty = Pretty;
    37   structure Pretty = Pretty;
    38 end;
    38 end;