# HG changeset patch
# User narasche
# Date 878648977 -3600
# Node ID 57c1e7d709601529285bf98f1d0f70f851185e17
# Parent  de6e388f3d8692e37e4dba8597b5925797b867c3
data kinds 'datatypes', data kinds 'records' added

diff -r de6e388f3d86 -r 57c1e7d70960 src/HOL/thy_data.ML
--- a/src/HOL/thy_data.ML	Tue Nov 04 13:35:13 1997 +0100
+++ b/src/HOL/thy_data.ML	Tue Nov 04 14:09:37 1997 +0100
@@ -17,6 +17,9 @@
 
 signature THY_DATA =
 sig
+  val datatypesK: string;
+  val get_record_data: theory -> ((string * (string * ctyp) list) Symtab.table);
+  val put_record_data: ((string * (string * ctyp) list) Symtab.table) -> theory -> theory;
   val get_datatypes_sg: Sign.sg -> datatype_info Symtab.table
   val get_datatypes: theory -> datatype_info Symtab.table
   val put_datatypes: datatype_info Symtab.table -> theory -> theory
@@ -46,33 +49,68 @@
     Pretty.writeln (Pretty.strs ("datatypes:" :: map fst (Symtab.dest tab)));
 in
   val datatypes_thy_data = (datatypesK, (empty, prep_ext, merge, print));
+  (* get and put datatypes *)
+
+  fun get_datatypes_sg sg =
+    (case Sign.get_data sg datatypesK of
+      DatatypeInfo tab => tab
+    | _ => sys_error "get_datatypes_sg");
+
+  val get_datatypes = get_datatypes_sg o sign_of;
+
+  fun put_datatypes tab thy =
+    Theory.put_data (datatypesK, DatatypeInfo tab) thy;
 end;
 
 
-(* get and put datatypes *)
+(** records **)
+
+(* data kind 'records' *)
+
+(* methods *)
+
+local
 
-fun get_datatypes_sg sg =
-  (case Sign.get_data sg datatypesK of
-    DatatypeInfo tab => tab
-  | _ => sys_error "get_datatypes_sg");
+  val recordsK = "records";
+  exception Records of
+    (string * (string * ctyp) list) Symtab.table;
+
+  fun forget_Records (Records t) = t; (* FIXME *) (* not very nice *)
 
-val get_datatypes = get_datatypes_sg o sign_of;
+  val empty = Records Symtab.null;
+
+  fun prep_ext r = r;
+
+  fun merge (Records rs1, Records rs2) = Records (Symtab.merge (fn (a,b) => true) (rs1, rs2));
 
-fun put_datatypes tab thy =
-  Theory.put_data (datatypesK, DatatypeInfo tab) thy;
-
-
+  fun print_aux (record_name, (parent, (sels_types))) = 
+     let val sel_types_string = 
+             (map (fn (sel,sel_type) => Pretty.block([Pretty.str (sel ^ " :: "), 
+                                                    Pretty.quote (Pretty.str (Display.string_of_ctyp sel_type))])));
+      in
+      Pretty.big_list ("record " ^ record_name ^ " =")
+                      (if parent = "" then (sel_types_string sels_types)
+                                      else (Pretty.str (parent ^ " +")) :: (sel_types_string sels_types))
+      end;
 
-(** records **)         (* FIXME *)
+  fun print (Records rs) =
+      if (Symtab.is_null rs) then
+        Pretty.writeln (Pretty.str ("no records available")) else
+        let val data = (Symtab.dest rs) in
+           seq Pretty.writeln (map print_aux data)
+        end;
+  in
 
-val recordsK = "records";
+  val record_thy_data = (recordsK, (empty, prep_ext, merge, print));
+  fun get_record_data thy  = forget_Records(Theory.get_data thy recordsK);
+  fun put_record_data rd = Theory.put_data (recordsK, Records rd);
 
+  end;
 
 
 (** hol_data **)
 
 val hol_data =
- [Simplifier.simpset_thy_data, ClasetThyData.thy_data, datatypes_thy_data];
-
+ [Simplifier.simpset_thy_data, ClasetThyData.thy_data, datatypes_thy_data, record_thy_data];
 
 end;