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