equal
deleted
inserted
replaced
1 theory StoringData |
1 theory StoringData |
2 imports "../Base" |
2 imports "../Base" |
3 begin |
3 begin |
4 |
4 |
5 section {* Storing Data *} |
5 section {* Storing Data\label{recipe:storingdata} *} |
6 |
6 |
7 |
7 |
8 text {* |
8 text {* |
9 {\bf Problem:} |
9 {\bf Problem:} |
10 Your tool needs to keep complex data.\smallskip |
10 Your tool needs to keep complex data.\smallskip |
14 Every generic data slot may keep data of any kind which is stored in the |
14 Every generic data slot may keep data of any kind which is stored in the |
15 context. |
15 context. |
16 |
16 |
17 *} |
17 *} |
18 |
18 |
19 ML {* |
19 ML {* local |
20 local |
|
21 |
20 |
22 structure Data = GenericDataFun |
21 structure Data = GenericDataFun |
23 ( |
22 ( |
24 type T = int Symtab.table |
23 type T = int Symtab.table |
25 val empty = Symtab.empty |
24 val empty = Symtab.empty |
31 |
30 |
32 val lookup = Symtab.lookup o Data.get |
31 val lookup = Symtab.lookup o Data.get |
33 |
32 |
34 fun update k v = Data.map (Symtab.update (k, v)) |
33 fun update k v = Data.map (Symtab.update (k, v)) |
35 |
34 |
36 end |
35 end *} |
37 *} |
|
38 |
36 |
39 setup {* Context.theory_map (update "foo" 1) *} |
37 setup {* Context.theory_map (update "foo" 1) *} |
40 |
38 |
41 ML {* lookup (Context.Proof @{context}) "foo" *} |
39 ML {* lookup (Context.Proof @{context}) "foo" *} |
42 |
40 |