equal
deleted
inserted
replaced
5 section {* Storing Data\label{recipe:storingdata} *} |
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 manage data.\smallskip |
11 |
11 |
12 {\bf Solution:} This can be achieved using a generic data slot.\smallskip |
12 {\bf Solution:} This can be achieved using a generic data slot.\smallskip |
13 |
13 |
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 {* local |
19 ML {* |
|
20 local |
20 |
21 |
21 structure Data = GenericDataFun |
22 structure Data = GenericDataFun |
22 ( |
23 ( type T = int Symtab.table |
23 type T = int Symtab.table |
24 val empty = Symtab.empty |
24 val empty = Symtab.empty |
25 val extend = I |
25 val extend = I |
26 fun merge _ = Symtab.merge (K true) |
26 fun merge _ = Symtab.merge (K true) |
27 ) |
27 ) |
|
28 |
28 |
29 in |
29 in |
30 |
30 |
31 val lookup = Symtab.lookup o Data.get |
31 val lookup = Symtab.lookup o Data.get |
32 |
32 |
34 |
34 |
35 end *} |
35 end *} |
36 |
36 |
37 setup {* Context.theory_map (update "foo" 1) *} |
37 setup {* Context.theory_map (update "foo" 1) *} |
38 |
38 |
39 ML {* lookup (Context.Proof @{context}) "foo" *} |
39 text {* |
|
40 |
|
41 @{ML_response [display] "lookup (Context.Proof @{context}) \"foo\"" "SOME 1"} |
|
42 |
|
43 |
|
44 *} |
40 |
45 |
41 text {* |
46 text {* |
42 alternatives: TheoryDataFun, ProofDataFun |
47 alternatives: TheoryDataFun, ProofDataFun |
43 Code: Pure/context.ML *} |
48 Code: Pure/context.ML *} |
44 |
49 |