|
61
|
1 |
theory StoringData
|
|
|
2 |
imports "../Base"
|
|
|
3 |
begin
|
|
|
4 |
|
|
63
|
5 |
section {* Storing Data\label{recipe:storingdata} *}
|
|
61
|
6 |
|
|
|
7 |
|
|
|
8 |
text {*
|
|
|
9 |
{\bf Problem:}
|
|
|
10 |
Your tool needs to keep complex data.\smallskip
|
|
|
11 |
|
|
|
12 |
{\bf Solution:} This can be achieved using a generic data slot.\smallskip
|
|
|
13 |
|
|
|
14 |
Every generic data slot may keep data of any kind which is stored in the
|
|
|
15 |
context.
|
|
|
16 |
|
|
|
17 |
*}
|
|
|
18 |
|
|
63
|
19 |
ML {* local
|
|
61
|
20 |
|
|
|
21 |
structure Data = GenericDataFun
|
|
|
22 |
(
|
|
|
23 |
type T = int Symtab.table
|
|
|
24 |
val empty = Symtab.empty
|
|
|
25 |
val extend = I
|
|
|
26 |
fun merge _ = Symtab.merge (K true)
|
|
|
27 |
)
|
|
|
28 |
|
|
|
29 |
in
|
|
|
30 |
|
|
|
31 |
val lookup = Symtab.lookup o Data.get
|
|
|
32 |
|
|
|
33 |
fun update k v = Data.map (Symtab.update (k, v))
|
|
|
34 |
|
|
63
|
35 |
end *}
|
|
61
|
36 |
|
|
|
37 |
setup {* Context.theory_map (update "foo" 1) *}
|
|
|
38 |
|
|
|
39 |
ML {* lookup (Context.Proof @{context}) "foo" *}
|
|
|
40 |
|
|
|
41 |
text {*
|
|
|
42 |
alternatives: TheoryDataFun, ProofDataFun
|
|
|
43 |
Code: Pure/context.ML *}
|
|
|
44 |
|
|
|
45 |
end |