| author | Christian Urban <urbanc@in.tum.de> |
| Wed, 14 Jan 2009 16:46:07 +0000 | |
| changeset 68 | e7519207c2b7 |
| parent 63 | 83cea5dc6bac |
| child 69 | 19106a9975c1 |
| permissions | -rw-r--r-- |
| 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:}
|
|
|
68
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
10 |
Your tool needs to manage data.\smallskip |
| 61 | 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 |
||
|
68
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
19 |
ML {*
|
|
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
20 |
local |
| 61 | 21 |
|
22 |
structure Data = GenericDataFun |
|
|
68
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
23 |
( type T = int Symtab.table |
|
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
24 |
val empty = Symtab.empty |
|
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
25 |
val extend = I |
|
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
26 |
fun merge _ = Symtab.merge (K true) |
|
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
27 |
) |
| 61 | 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 |
||
|
68
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
39 |
text {*
|
|
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
40 |
|
|
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
41 |
@{ML_response [display] "lookup (Context.Proof @{context}) \"foo\"" "SOME 1"}
|
|
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
42 |
|
|
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
43 |
|
|
e7519207c2b7
added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents:
63
diff
changeset
|
44 |
*} |
| 61 | 45 |
|
46 |
text {*
|
|
47 |
alternatives: TheoryDataFun, ProofDataFun |
|
48 |
Code: Pure/context.ML *} |
|
49 |
||
50 |
end |