src/Pure/Isar/proof_data.ML
changeset 16530 3e493fa130a3
parent 16529 d4de40568ab1
child 16531 9b442d0e5c0c
     1.1 --- a/src/Pure/Isar/proof_data.ML	Wed Jun 22 18:26:28 2005 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,48 +0,0 @@
     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: ProofContext.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: ProofContext.context -> unit
    1.24 -  val get: ProofContext.context -> T
    1.25 -  val put: T -> ProofContext.context -> ProofContext.context
    1.26 -  val map: (T -> T) -> ProofContext.context -> ProofContext.context
    1.27 -end;
    1.28 -
    1.29 -functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
    1.30 -struct
    1.31 -
    1.32 -(*object kind kept private!*)
    1.33 -val kind = Object.kind Args.name;
    1.34 -
    1.35 -type T = Args.T;
    1.36 -exception Data of T;
    1.37 -
    1.38 -val init =
    1.39 -  ProofContext.init_data kind
    1.40 -    (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x);
    1.41 -
    1.42 -val print = ProofContext.print_data kind;
    1.43 -val get = ProofContext.get_data kind (fn Data x => x);
    1.44 -val put = ProofContext.put_data kind Data;
    1.45 -fun map f ctxt = put (f (get ctxt)) ctxt;
    1.46 -
    1.47 -end;
    1.48 -
    1.49 -
    1.50 -(*hide private data access functions*)
    1.51 -structure ProofContext: PROOF_CONTEXT = ProofContext;