# HG changeset patch
# User wenzelm
# Date 876921179 -7200
# Node ID a5839ecee7b84e610543c6a7b4fd778f8977e1ef
# Parent  8b1b0d493ca928c172b648fcdd77b43ad3ac2d7b
tuned;
prepare ext;

diff -r 8b1b0d493ca9 -r a5839ecee7b8 src/Pure/data.ML
--- a/src/Pure/data.ML	Wed Oct 15 11:43:27 1997 +0200
+++ b/src/Pure/data.ML	Wed Oct 15 15:12:59 1997 +0200
@@ -11,26 +11,38 @@
   type T
   val empty: T
   val merge: T * T -> T
-  val print: T -> unit
-  val init: T -> string -> exn -> (exn * exn -> exn) -> (string -> exn -> Pretty.T) -> T
+  val prep_ext: T -> T
+  val kinds: T -> string list
+  val init: T -> string -> exn -> (exn -> exn) -> (exn * exn -> exn)
+    -> (string -> exn -> unit) -> T
   val get: T -> string -> exn
   val put: T -> string -> exn -> T
+  val print: T -> string -> unit
 end;
 
 
 structure Data: DATA =
 struct
 
+
 (* datatype T *)
 
-datatype T = Data of (*value, merge method, pp method*)
-  (exn * ((exn * exn -> exn) * (string -> exn -> Pretty.T))) Symtab.table;
+datatype T = Data of
+  (exn *				(*value*)
+   ((exn -> exn) *			(*prepare extend method*)
+    (exn * exn -> exn) *		(*merge and prepare extend method*)
+    (string -> exn -> unit)))		(*print method*)
+  Symtab.table;
+
+val empty = Data Symtab.null;
+
+fun kinds (Data tab) = map fst (Symtab.dest tab);
 
 
 (* errors *)
 
-fun err_msg_merge kind =
-  error_msg ("Error while trying to merge " ^ quote kind ^ " data");
+fun err_mergext kind =
+  error ("Error while extend / merge of " ^ quote kind ^ " data");
 
 fun err_dup_init kind =
   error ("Duplicate initialization of " ^ quote kind ^ " data");
@@ -39,10 +51,7 @@
   error ("Tried to access uninitialized " ^ quote kind ^ " data");
 
 
-(* operations *)
-
-val empty = Data Symtab.null;
-
+(* prepare data *)
 
 fun merge (Data tab1, Data tab2) =
   let
@@ -56,36 +65,37 @@
        None => []
      | Some x => [(kind, x)]);
 
-    fun merge_entries [x] = x
-      | merge_entries [(kind, (e1, mths as (mrg, _))), (_, (e2, _))] =
-          (kind, (mrg (e1, e2) handle exn => (err_msg_merge kind; raise exn), mths))
+    fun merge_entries [(kind, (e, mths as (ext, _, _)))] =
+          (kind, (ext e handle exn => err_mergext kind, mths))
+      | merge_entries [(kind, (e1, mths as (_, mrg, _))), (_, (e2, _))] =
+          (kind, (mrg (e1, e2) handle exn => (err_mergext kind; raise exn), mths))
       | merge_entries _ = sys_error "merge_entries";
 
     val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds;
   in Data (Symtab.make data) end;
 
 
-fun print (Data tab) =
-  let fun prnt (kind, (e, (_, prt))) = Pretty.writeln (prt kind e) in
-    seq prnt (Symtab.dest tab)
-  end;
+fun prep_ext data = merge (data, empty);		(* FIXME !? *)
 
-
-fun init (Data tab) kind e mrg prt =
-  Data (Symtab.update_new ((kind, (e, (mrg, prt))), tab))
+fun init (Data tab) kind e ext mrg prt =
+  Data (Symtab.update_new ((kind, (e, (ext, mrg, prt))), tab))
     handle Symtab.DUPLICATE _ => err_dup_init kind;
 
 
-fun get (Data tab) kind =
+(* access data *)
+
+fun lookup tab kind =
   (case Symtab.lookup (tab, kind) of
-    Some (e, _) => e
+    Some x => x
   | None => err_uninit kind);
 
+fun get (Data tab) kind = fst (lookup tab kind);
 
 fun put (Data tab) kind e =
-  (case Symtab.lookup (tab, kind) of
-    Some (_, meths) => Data (Symtab.update ((kind, (e, meths)), tab))
-  | None => err_uninit kind);
+  Data (Symtab.update ((kind, (e, snd (lookup tab kind))), tab));
+
+fun print (Data tab) kind =
+  let val (e, (_, _, prt)) = lookup tab kind in prt kind e end;
 
 
 end;