# HG changeset patch # User wenzelm # Date 910621906 -3600 # Node ID 262ce90e47369b70cfdb5810197787b89dd37287 # Parent ff3c82b4760339e30bf47cd9946fc952dd26b435 Type-safe interface for proof context data. diff -r ff3c82b47603 -r 262ce90e4736 src/Pure/Isar/proof_data.ML --- /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;