| author | paulson |
| Fri, 21 Apr 2000 11:29:57 +0200 | |
| changeset 8759 | 49154c960140 |
| parent 6644 | 123b215882ae |
| child 9095 | 3b26cc949016 |
| permissions | -rw-r--r-- |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
1 |
|
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
2 |
Pure/General/ |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
3 |
|
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
4 |
|
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
5 |
This directory contains general purpose modules, all of which are |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
6 |
exported. |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
7 |
|
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
8 |
TableFun (generic tables) |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
9 |
Symtab (tables indexed by strings) |
| 6135 | 10 |
GraphFun (generic directed graphs) |
11 |
Graph (graphs indexed by strings) |
|
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
12 |
Object (generic objects of arbitrary type) |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
13 |
Seq (unbounded sequences) |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
14 |
NameSpace (hierarchically structured name spaces) |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
15 |
Position (input positions) |
| 6634 | 16 |
Scan (generic scanner toolbox) |
| 6644 | 17 |
Source (co-algebraic data sources) |
18 |
Symbol (generalized characters) |
|
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
19 |
Path (abstract algebra of file paths) |
| 6644 | 20 |
Url (basic URL support) |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
21 |
File (file system operations) |
| 6317 | 22 |
Buffer (simple string buffers) |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
23 |
History (histories of values, with undo and redo) |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
24 |
Pretty (generic pretty printing module) |