Type-safe interface for proof context data.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/proof_data.ML Mon Nov 09 15:31:46 1998 +0100
@@ -0,0 +1,47 @@
+(* Title: Pure/Isar/proof_data.ML
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+
+Type-safe interface for proof context data.
+*)
+
+signature PROOF_DATA_ARGS =
+sig
+ val name: string
+ type T
+ val init: theory -> T
+ val print: Proof.context -> T -> unit
+end;
+
+signature PROOF_DATA =
+sig
+ type T
+ val init: theory -> theory
+ val print: Proof.context -> unit
+ val get: Proof.context -> T
+ val put: T -> Proof.context -> Proof.context
+end;
+
+functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
+struct
+
+(*object kind kept private!*)
+val kind = Object.kind Args.name;
+
+type T = Args.T;
+exception Data of T;
+
+val init =
+ ProofContext.init_data kind
+ (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x);
+
+val print = ProofContext.print_data kind;
+val get = ProofContext.get_data kind (fn Data x => x);
+val put = ProofContext.put_data kind Data;
+
+end;
+
+
+(*hide private data access functions*)
+structure ProofContext: PROOF_CONTEXT = ProofContext;
+structure Proof: PROOF = Proof;