src/Pure/context.ML
changeset 33517 d064fa48f305
parent 33033 fcc77a029bb2
child 33606 2b27020ffcb2
     1.1 --- a/src/Pure/context.ML	Sun Nov 08 14:44:31 2009 +0100
     1.2 +++ b/src/Pure/context.ML	Sun Nov 08 16:27:50 2009 +0100
     1.3 @@ -572,7 +572,7 @@
     1.4  
     1.5  (** theory data **)
     1.6  
     1.7 -signature THEORY_DATA_ARGS =
     1.8 +signature OLD_THEORY_DATA_ARGS =
     1.9  sig
    1.10    type T
    1.11    val empty: T
    1.12 @@ -581,7 +581,7 @@
    1.13    val merge: Pretty.pp -> T * T -> T
    1.14  end;
    1.15  
    1.16 -signature THEORY_DATA =
    1.17 +signature OLD_THEORY_DATA =
    1.18  sig
    1.19    type T
    1.20    val get: theory -> T
    1.21 @@ -590,7 +590,7 @@
    1.22    val init: theory -> theory
    1.23  end;
    1.24  
    1.25 -functor TheoryDataFun(Data: THEORY_DATA_ARGS): THEORY_DATA =
    1.26 +functor TheoryDataFun(Data: OLD_THEORY_DATA_ARGS): OLD_THEORY_DATA =
    1.27  struct
    1.28  
    1.29  type T = Data.T;
    1.30 @@ -610,6 +610,38 @@
    1.31  
    1.32  end;
    1.33  
    1.34 +signature THEORY_DATA_ARGS =
    1.35 +sig
    1.36 +  type T
    1.37 +  val empty: T
    1.38 +  val extend: T -> T
    1.39 +  val merge: T * T -> T
    1.40 +end;
    1.41 +
    1.42 +signature THEORY_DATA =
    1.43 +sig
    1.44 +  type T
    1.45 +  val get: theory -> T
    1.46 +  val put: T -> theory -> theory
    1.47 +  val map: (T -> T) -> theory -> theory
    1.48 +end;
    1.49 +
    1.50 +functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
    1.51 +struct
    1.52 +
    1.53 +structure Result = TheoryDataFun
    1.54 +(
    1.55 +  type T = Data.T;
    1.56 +  val empty = Data.empty;
    1.57 +  val copy = I;
    1.58 +  val extend = Data.extend;
    1.59 +  fun merge _ = Data.merge;
    1.60 +);
    1.61 +
    1.62 +open Result;
    1.63 +
    1.64 +end;
    1.65 +
    1.66  
    1.67  
    1.68  (** proof data **)
    1.69 @@ -628,7 +660,7 @@
    1.70    val map: (T -> T) -> Proof.context -> Proof.context
    1.71  end;
    1.72  
    1.73 -functor ProofDataFun(Data: PROOF_DATA_ARGS): PROOF_DATA =
    1.74 +functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA =
    1.75  struct
    1.76  
    1.77  type T = Data.T;
    1.78 @@ -651,7 +683,7 @@
    1.79    type T
    1.80    val empty: T
    1.81    val extend: T -> T
    1.82 -  val merge: Pretty.pp -> T * T -> T
    1.83 +  val merge: T * T -> T
    1.84  end;
    1.85  
    1.86  signature GENERIC_DATA =
    1.87 @@ -662,11 +694,11 @@
    1.88    val map: (T -> T) -> Context.generic -> Context.generic
    1.89  end;
    1.90  
    1.91 -functor GenericDataFun(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
    1.92 +functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
    1.93  struct
    1.94  
    1.95 -structure Thy_Data = TheoryDataFun(open Data val copy = I);
    1.96 -structure Prf_Data = ProofDataFun(type T = Data.T val init = Thy_Data.get);
    1.97 +structure Thy_Data = Theory_Data(Data);
    1.98 +structure Prf_Data = Proof_Data(type T = Data.T val init = Thy_Data.get);
    1.99  
   1.100  type T = Data.T;
   1.101