src/Pure/Isar/proof_data.ML
author wenzelm
Fri Jun 04 19:55:26 1999 +0200 (1999-06-04 ago)
changeset 6777 175ff298ac0e
parent 5821 262ce90e4736
child 6788 6eaf6856ee4a
permissions -rw-r--r--
added put_st;
     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   val put_st: T -> Proof.state -> Proof.state
    24 end;
    25 
    26 functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
    27 struct
    28 
    29 (*object kind kept private!*)
    30 val kind = Object.kind Args.name;
    31 
    32 type T = Args.T;
    33 exception Data of T;
    34 
    35 val init =
    36   ProofContext.init_data kind
    37     (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x);
    38 
    39 val print = ProofContext.print_data kind;
    40 val get = ProofContext.get_data kind (fn Data x => x);
    41 val put = ProofContext.put_data kind Data;
    42 val put_st = Proof.put_data kind Data;
    43 
    44 end;
    45 
    46 
    47 (*hide private data access functions*)
    48 structure ProofContext: PROOF_CONTEXT = ProofContext;
    49 structure Proof: PROOF = Proof;