src/Pure/Isar/proof_data.ML
author wenzelm
Fri Apr 07 17:36:25 2000 +0200 (2000-04-07 ago)
changeset 8681 957a5fe9b212
parent 8143 b0e44ab73631
child 8807 0046be1769f9
permissions -rw-r--r--
apply etc.: comments;
     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 map: (T -> T) -> Proof.context -> Proof.context
    24   val get_st: Proof.state -> T
    25   val put_st: T -> Proof.state -> Proof.state
    26   val map_st: (T -> T) -> Proof.state -> Proof.state
    27 end;
    28 
    29 functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
    30 struct
    31 
    32 (*object kind kept private!*)
    33 val kind = Object.kind Args.name;
    34 
    35 type T = Args.T;
    36 exception Data of T;
    37 
    38 val init =
    39   ProofContext.init_data kind
    40     (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x);
    41 
    42 val print = ProofContext.print_data kind;
    43 val get = ProofContext.get_data kind (fn Data x => x);
    44 val put = ProofContext.put_data kind Data;
    45 fun map f ctxt = put (f (get ctxt)) ctxt;
    46 
    47 val get_st = get o Proof.context_of;
    48 val put_st = Proof.put_data kind Data;
    49 fun map_st f st = put_st (f (get_st st)) st;
    50 
    51 end;
    52 
    53 
    54 (*hide private data access functions*)
    55 structure ProofContext: PROOF_CONTEXT = ProofContext;
    56 structure Proof: PROOF = Proof;