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