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