src/Pure/Isar/proof_data.ML
author wenzelm
Fri Mar 19 11:24:00 1999 +0100 (1999-03-19)
changeset 6404 2daaf2943c79
parent 5821 262ce90e4736
child 6777 175ff298ac0e
permissions -rw-r--r--
common qed and end of proofs;
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@5821
    23
end;
wenzelm@5821
    24
wenzelm@5821
    25
functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
wenzelm@5821
    26
struct
wenzelm@5821
    27
wenzelm@5821
    28
(*object kind kept private!*)
wenzelm@5821
    29
val kind = Object.kind Args.name;
wenzelm@5821
    30
wenzelm@5821
    31
type T = Args.T;
wenzelm@5821
    32
exception Data of T;
wenzelm@5821
    33
wenzelm@5821
    34
val init =
wenzelm@5821
    35
  ProofContext.init_data kind
wenzelm@5821
    36
    (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x);
wenzelm@5821
    37
wenzelm@5821
    38
val print = ProofContext.print_data kind;
wenzelm@5821
    39
val get = ProofContext.get_data kind (fn Data x => x);
wenzelm@5821
    40
val put = ProofContext.put_data kind Data;
wenzelm@5821
    41
wenzelm@5821
    42
end;
wenzelm@5821
    43
wenzelm@5821
    44
wenzelm@5821
    45
(*hide private data access functions*)
wenzelm@5821
    46
structure ProofContext: PROOF_CONTEXT = ProofContext;
wenzelm@5821
    47
structure Proof: PROOF = Proof;