src/Pure/Isar/proof_data.ML
author wenzelm
Mon Nov 09 15:31:46 1998 +0100 (1998-11-09 ago)
changeset 5821 262ce90e4736
child 6777 175ff298ac0e
permissions -rw-r--r--
Type-safe interface for proof context data.
     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: Proof.context -> T -> unit
    14 end;
    15 
    16 signature PROOF_DATA =
    17 sig
    18   type T
    19   val init: theory -> theory
    20   val print: Proof.context -> unit
    21   val get: Proof.context -> T
    22   val put: T -> Proof.context -> Proof.context
    23 end;
    24 
    25 functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
    26 struct
    27 
    28 (*object kind kept private!*)
    29 val kind = Object.kind Args.name;
    30 
    31 type T = Args.T;
    32 exception Data of T;
    33 
    34 val init =
    35   ProofContext.init_data kind
    36     (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x);
    37 
    38 val print = ProofContext.print_data kind;
    39 val get = ProofContext.get_data kind (fn Data x => x);
    40 val put = ProofContext.put_data kind Data;
    41 
    42 end;
    43 
    44 
    45 (*hide private data access functions*)
    46 structure ProofContext: PROOF_CONTEXT = ProofContext;
    47 structure Proof: PROOF = Proof;