src/Pure/Isar/proof_data.ML
changeset 5821 262ce90e4736
child 6777 175ff298ac0e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/proof_data.ML	Mon Nov 09 15:31:46 1998 +0100
     1.3 @@ -0,0 +1,47 @@
     1.4 +(*  Title:      Pure/Isar/proof_data.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Type-safe interface for proof context data.
     1.9 +*)
    1.10 +
    1.11 +signature PROOF_DATA_ARGS =
    1.12 +sig
    1.13 +  val name: string
    1.14 +  type T
    1.15 +  val init: theory -> T
    1.16 +  val print: Proof.context -> T -> unit
    1.17 +end;
    1.18 +
    1.19 +signature PROOF_DATA =
    1.20 +sig
    1.21 +  type T
    1.22 +  val init: theory -> theory
    1.23 +  val print: Proof.context -> unit
    1.24 +  val get: Proof.context -> T
    1.25 +  val put: T -> Proof.context -> Proof.context
    1.26 +end;
    1.27 +
    1.28 +functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
    1.29 +struct
    1.30 +
    1.31 +(*object kind kept private!*)
    1.32 +val kind = Object.kind Args.name;
    1.33 +
    1.34 +type T = Args.T;
    1.35 +exception Data of T;
    1.36 +
    1.37 +val init =
    1.38 +  ProofContext.init_data kind
    1.39 +    (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x);
    1.40 +
    1.41 +val print = ProofContext.print_data kind;
    1.42 +val get = ProofContext.get_data kind (fn Data x => x);
    1.43 +val put = ProofContext.put_data kind Data;
    1.44 +
    1.45 +end;
    1.46 +
    1.47 +
    1.48 +(*hide private data access functions*)
    1.49 +structure ProofContext: PROOF_CONTEXT = ProofContext;
    1.50 +structure Proof: PROOF = Proof;