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.);
wenzelm@5821
     1
(*  Title:      Pure/Isar/proof_data.ML
wenzelm@5821
     2
    ID:         $Id$
wenzelm@5821
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8807
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@5821
     5
wenzelm@5821
     6
Type-safe interface for proof context data.
wenzelm@5821
     7
*)
wenzelm@5821
     8
wenzelm@5821
     9
signature PROOF_DATA_ARGS =
wenzelm@5821
    10
sig
wenzelm@5821
    11
  val name: string
wenzelm@5821
    12
  type T
wenzelm@5821
    13
  val init: theory -> T
wenzelm@5821
    14
  val print: Proof.context -> T -> unit
wenzelm@5821
    15
end;
wenzelm@5821
    16
wenzelm@5821
    17
signature PROOF_DATA =
wenzelm@5821
    18
sig
wenzelm@5821
    19
  type T
wenzelm@5821
    20
  val init: theory -> theory
wenzelm@5821
    21
  val print: Proof.context -> unit
wenzelm@5821
    22
  val get: Proof.context -> T
wenzelm@5821
    23
  val put: T -> Proof.context -> Proof.context
wenzelm@8143
    24
  val map: (T -> T) -> Proof.context -> Proof.context
wenzelm@6788
    25
  val get_st: Proof.state -> T
wenzelm@6777
    26
  val put_st: T -> Proof.state -> Proof.state
wenzelm@8143
    27
  val map_st: (T -> T) -> Proof.state -> Proof.state
wenzelm@5821
    28
end;
wenzelm@5821
    29
wenzelm@5821
    30
functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
wenzelm@5821
    31
struct
wenzelm@5821
    32
wenzelm@5821
    33
(*object kind kept private!*)
wenzelm@5821
    34
val kind = Object.kind Args.name;
wenzelm@5821
    35
wenzelm@5821
    36
type T = Args.T;
wenzelm@5821
    37
exception Data of T;
wenzelm@5821
    38
wenzelm@5821
    39
val init =
wenzelm@5821
    40
  ProofContext.init_data kind
wenzelm@5821
    41
    (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x);
wenzelm@5821
    42
wenzelm@5821
    43
val print = ProofContext.print_data kind;
wenzelm@5821
    44
val get = ProofContext.get_data kind (fn Data x => x);
wenzelm@5821
    45
val put = ProofContext.put_data kind Data;
wenzelm@8143
    46
fun map f ctxt = put (f (get ctxt)) ctxt;
wenzelm@8143
    47
wenzelm@6788
    48
val get_st = get o Proof.context_of;
wenzelm@6777
    49
val put_st = Proof.put_data kind Data;
wenzelm@8143
    50
fun map_st f st = put_st (f (get_st st)) st;
wenzelm@5821
    51
wenzelm@5821
    52
end;
wenzelm@5821
    53
wenzelm@5821
    54
wenzelm@5821
    55
(*hide private data access functions*)
wenzelm@5821
    56
structure ProofContext: PROOF_CONTEXT = ProofContext;
wenzelm@5821
    57
structure Proof: PROOF = Proof;