# HG changeset patch
# User wenzelm
# Date 1257694070 -3600
# Node ID d064fa48f3051bfc963f9c581f9e1e6fcfe18b60
# Parent  0855a09bc5cfcb6895152eac7291ceccd28121d2
modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;

diff -r 0855a09bc5cf -r d064fa48f305 src/Pure/context.ML
--- a/src/Pure/context.ML	Sun Nov 08 14:44:31 2009 +0100
+++ b/src/Pure/context.ML	Sun Nov 08 16:27:50 2009 +0100
@@ -572,7 +572,7 @@
 
 (** theory data **)
 
-signature THEORY_DATA_ARGS =
+signature OLD_THEORY_DATA_ARGS =
 sig
   type T
   val empty: T
@@ -581,7 +581,7 @@
   val merge: Pretty.pp -> T * T -> T
 end;
 
-signature THEORY_DATA =
+signature OLD_THEORY_DATA =
 sig
   type T
   val get: theory -> T
@@ -590,7 +590,7 @@
   val init: theory -> theory
 end;
 
-functor TheoryDataFun(Data: THEORY_DATA_ARGS): THEORY_DATA =
+functor TheoryDataFun(Data: OLD_THEORY_DATA_ARGS): OLD_THEORY_DATA =
 struct
 
 type T = Data.T;
@@ -610,6 +610,38 @@
 
 end;
 
+signature THEORY_DATA_ARGS =
+sig
+  type T
+  val empty: T
+  val extend: T -> T
+  val merge: T * T -> T
+end;
+
+signature THEORY_DATA =
+sig
+  type T
+  val get: theory -> T
+  val put: T -> theory -> theory
+  val map: (T -> T) -> theory -> theory
+end;
+
+functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
+struct
+
+structure Result = TheoryDataFun
+(
+  type T = Data.T;
+  val empty = Data.empty;
+  val copy = I;
+  val extend = Data.extend;
+  fun merge _ = Data.merge;
+);
+
+open Result;
+
+end;
+
 
 
 (** proof data **)
@@ -628,7 +660,7 @@
   val map: (T -> T) -> Proof.context -> Proof.context
 end;
 
-functor ProofDataFun(Data: PROOF_DATA_ARGS): PROOF_DATA =
+functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA =
 struct
 
 type T = Data.T;
@@ -651,7 +683,7 @@
   type T
   val empty: T
   val extend: T -> T
-  val merge: Pretty.pp -> T * T -> T
+  val merge: T * T -> T
 end;
 
 signature GENERIC_DATA =
@@ -662,11 +694,11 @@
   val map: (T -> T) -> Context.generic -> Context.generic
 end;
 
-functor GenericDataFun(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
+functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
 struct
 
-structure Thy_Data = TheoryDataFun(open Data val copy = I);
-structure Prf_Data = ProofDataFun(type T = Data.T val init = Thy_Data.get);
+structure Thy_Data = Theory_Data(Data);
+structure Prf_Data = Proof_Data(type T = Data.T val init = Thy_Data.get);
 
 type T = Data.T;