src/Pure/Isar/proof_data.ML
author wenzelm
Wed Dec 05 03:18:03 2001 +0100 (2001-12-05 ago)
changeset 12385 389d11fb62c8
parent 8807 0046be1769f9
child 13379 a21e132c3304
permissions -rw-r--r--
removed unused functionality (weight etc.);
     1 (*  Title:      Pure/Isar/proof_data.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Type-safe interface for proof context data.
     7 *)
     8 
     9 signature PROOF_DATA_ARGS =
    10 sig
    11   val name: string
    12   type T
    13   val init: theory -> T
    14   val print: Proof.context -> T -> unit
    15 end;
    16 
    17 signature PROOF_DATA =
    18 sig
    19   type T
    20   val init: theory -> theory
    21   val print: Proof.context -> unit
    22   val get: Proof.context -> T
    23   val put: T -> Proof.context -> Proof.context
    24   val map: (T -> T) -> Proof.context -> Proof.context
    25   val get_st: Proof.state -> T
    26   val put_st: T -> Proof.state -> Proof.state
    27   val map_st: (T -> T) -> Proof.state -> Proof.state
    28 end;
    29 
    30 functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
    31 struct
    32 
    33 (*object kind kept private!*)
    34 val kind = Object.kind Args.name;
    35 
    36 type T = Args.T;
    37 exception Data of T;
    38 
    39 val init =
    40   ProofContext.init_data kind
    41     (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x);
    42 
    43 val print = ProofContext.print_data kind;
    44 val get = ProofContext.get_data kind (fn Data x => x);
    45 val put = ProofContext.put_data kind Data;
    46 fun map f ctxt = put (f (get ctxt)) ctxt;
    47 
    48 val get_st = get o Proof.context_of;
    49 val put_st = Proof.put_data kind Data;
    50 fun map_st f st = put_st (f (get_st st)) st;
    51 
    52 end;
    53 
    54 
    55 (*hide private data access functions*)
    56 structure ProofContext: PROOF_CONTEXT = ProofContext;
    57 structure Proof: PROOF = Proof;