src/Pure/Isar/proof_data.ML
author wenzelm
Sat Sep 25 13:18:38 1999 +0200 (1999-09-25 ago)
changeset 7604 55566b9ec7d7
parent 6788 6eaf6856ee4a
child 8143 b0e44ab73631
permissions -rw-r--r--
tuned;
     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 get_st: Proof.state -> T
    24   val put_st: T -> Proof.state -> Proof.state
    25 end;
    26 
    27 functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
    28 struct
    29 
    30 (*object kind kept private!*)
    31 val kind = Object.kind Args.name;
    32 
    33 type T = Args.T;
    34 exception Data of T;
    35 
    36 val init =
    37   ProofContext.init_data kind
    38     (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x);
    39 
    40 val print = ProofContext.print_data kind;
    41 val get = ProofContext.get_data kind (fn Data x => x);
    42 val put = ProofContext.put_data kind Data;
    43 val get_st = get o Proof.context_of;
    44 val put_st = Proof.put_data kind Data;
    45 
    46 end;
    47 
    48 
    49 (*hide private data access functions*)
    50 structure ProofContext: PROOF_CONTEXT = ProofContext;
    51 structure Proof: PROOF = Proof;