equal
deleted
inserted
replaced
1 (* Title: Pure/Isar/proof_data.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 Type-safe interface for proof context data. |
|
6 *) |
|
7 |
|
8 signature PROOF_DATA_ARGS = |
|
9 sig |
|
10 val name: string |
|
11 type T |
|
12 val init: theory -> T |
|
13 val print: ProofContext.context -> T -> unit |
|
14 end; |
|
15 |
|
16 signature PROOF_DATA = |
|
17 sig |
|
18 type T |
|
19 val init: theory -> theory |
|
20 val print: ProofContext.context -> unit |
|
21 val get: ProofContext.context -> T |
|
22 val put: T -> ProofContext.context -> ProofContext.context |
|
23 val map: (T -> T) -> ProofContext.context -> ProofContext.context |
|
24 end; |
|
25 |
|
26 functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA = |
|
27 struct |
|
28 |
|
29 (*object kind kept private!*) |
|
30 val kind = Object.kind Args.name; |
|
31 |
|
32 type T = Args.T; |
|
33 exception Data of T; |
|
34 |
|
35 val init = |
|
36 ProofContext.init_data kind |
|
37 (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x); |
|
38 |
|
39 val print = ProofContext.print_data kind; |
|
40 val get = ProofContext.get_data kind (fn Data x => x); |
|
41 val put = ProofContext.put_data kind Data; |
|
42 fun map f ctxt = put (f (get ctxt)) ctxt; |
|
43 |
|
44 end; |
|
45 |
|
46 |
|
47 (*hide private data access functions*) |
|
48 structure ProofContext: PROOF_CONTEXT = ProofContext; |
|