changeset 6317 | 128e592f5489 |
parent 6222 | 2b24cf477313 |
child 6634 | 6f74e7aa5b4d |
--- a/src/Pure/General/ROOT.ML Tue Mar 09 12:08:50 1999 +0100 +++ b/src/Pure/General/ROOT.ML Tue Mar 09 12:09:05 1999 +0100 @@ -12,6 +12,7 @@ use "position.ML"; use "path.ML"; use "file.ML"; +use "buffer.ML"; use "history.ML"; use "scan.ML"; use "source.ML"; @@ -28,6 +29,7 @@ structure Position = Position; structure Path = Path; structure File = File; + structure Buffer = Buffer; structure History = History; structure Scan = Scan; structure Source = Source;