# HG changeset patch
# User wenzelm
# Date 897314250 -7200
# Node ID f73ad32e44d3f4ea080cb668800feea348c21d0c
# Parent  7b4c2a15373869cc6c9e4cfc6c9499ef801bbff8
Type-safe interface for theory data.

diff -r 7b4c2a153738 -r f73ad32e44d3 src/Pure/theory_data.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/theory_data.ML	Mon Jun 08 15:57:30 1998 +0200
@@ -0,0 +1,49 @@
+(*  Title:      Pure/theory_data.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Type-safe interface for theory data.
+*)
+
+signature THEORY_DATA_ARGS =
+sig
+  val name: string
+  type T
+  val empty: T
+  val prep_ext: T -> T
+  val merge: T * T -> T
+  val print: Sign.sg -> T -> unit
+end;
+
+signature THEORY_DATA =
+sig
+  type T
+  val init: theory -> theory
+  val print: theory -> unit
+  val get_sg: Sign.sg -> T
+  val get: theory -> T
+  val put: T -> theory -> theory
+end;
+
+functor TheoryDataFun(Args: THEORY_DATA_ARGS): THEORY_DATA =
+struct
+
+(*object kind kept private!*)
+val kind = Object.kind Args.name;
+
+type T = Args.T;
+exception Data of T;
+
+val init =
+  Theory.init_data kind
+    (Data Args.empty,
+      fn (Data x) => Data (Args.prep_ext x),
+      fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
+      fn sg => fn (Data x) => Args.print sg x);
+
+val print = Theory.print_data kind;
+val get_sg = Sign.get_data kind (fn Data x => x);
+val get = get_sg o Theory.sign_of;
+val put = Theory.put_data kind Data;
+
+end;