| author | wenzelm | 
| Fri, 02 Nov 2001 22:02:41 +0100 | |
| changeset 12021 | 8809efda06d3 | 
| parent 9119 | 8ca79837b41b | 
| child 12420 | a2a05c952b4d | 
| permissions | -rw-r--r-- | 
| 5018 | 1 | (* Title: Pure/General/ROOT.ML | 
| 2 | ID: $Id$ | |
| 3 | ||
| 9119 | 4 | Library of general tools --- prefer this over the 'Standard ML Library'. | 
| 5018 | 5 | *) | 
| 6 | ||
| 7 | use "table.ML"; | |
| 6134 | 8 | use "graph.ML"; | 
| 9119 | 9 | use "heap.ML"; | 
| 5018 | 10 | use "object.ML"; | 
| 11 | use "seq.ML"; | |
| 12 | use "name_space.ML"; | |
| 13 | use "position.ML"; | |
| 6634 | 14 | use "scan.ML"; | 
| 6638 | 15 | use "source.ML"; | 
| 16 | use "symbol.ML"; | |
| 5018 | 17 | use "path.ML"; | 
| 6638 | 18 | use "url.ML"; | 
| 5018 | 19 | use "file.ML"; | 
| 6317 | 20 | use "buffer.ML"; | 
| 5040 | 21 | use "history.ML"; | 
| 6116 
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
 wenzelm parents: 
5864diff
changeset | 22 | use "pretty.ML"; | 
| 5864 | 23 | |
| 24 | structure PureGeneral = | |
| 25 | struct | |
| 26 | structure Symtab = Symtab; | |
| 6136 | 27 | structure Graph = Graph; | 
| 5864 | 28 | structure Object = Object; | 
| 29 | structure Seq = Seq; | |
| 30 | structure NameSpace = NameSpace; | |
| 31 | structure Position = Position; | |
| 6634 | 32 | structure Scan = Scan; | 
| 6644 | 33 | structure Source = Source; | 
| 6638 | 34 | structure Symbol = Symbol; | 
| 5864 | 35 | structure Path = Path; | 
| 6638 | 36 | structure Url = Url; | 
| 5864 | 37 | structure File = File; | 
| 6317 | 38 | structure Buffer = Buffer; | 
| 5864 | 39 | structure History = History; | 
| 6116 
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
 wenzelm parents: 
5864diff
changeset | 40 | structure Pretty = Pretty; | 
| 5864 | 41 | end; |