discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
authorwenzelm
Mon Jan 04 23:20:35 2010 +0100 (2010-01-04)
changeset 342592ba492b8b6e8
parent 34258 e936d3c35ce0
child 34260 2524c1bbd087
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
NEWS
src/Pure/axclass.ML
src/Pure/context.ML
src/Pure/sign.ML
src/Pure/theory.ML
     1.1 --- a/NEWS	Mon Jan 04 22:43:07 2010 +0100
     1.2 +++ b/NEWS	Mon Jan 04 23:20:35 2010 +0100
     1.3 @@ -47,6 +47,11 @@
     1.4  * Subgoal.FOCUS (and variants): resulting goal state is normalized as
     1.5  usual for resolution.  Rare INCOMPATIBILITY.
     1.6  
     1.7 +* Discontinued old TheoryDataFun with its copy/init operation -- data
     1.8 +needs to be pure.  Functor Theory_Data_PP retains the traditional
     1.9 +Pretty.pp argument to merge, which is absent in the standard
    1.10 +Theory_Data version.
    1.11 +
    1.12  
    1.13  *** System ***
    1.14  
     2.1 --- a/src/Pure/axclass.ML	Mon Jan 04 22:43:07 2010 +0100
     2.2 +++ b/src/Pure/axclass.ML	Mon Jan 04 23:20:35 2010 +0100
     2.3 @@ -114,7 +114,7 @@
     2.4  
     2.5  (* setup data *)
     2.6  
     2.7 -structure AxClassData = TheoryDataFun
     2.8 +structure AxClassData = Theory_Data_PP
     2.9  (
    2.10    type T = axclasses * (instances * inst_params);
    2.11    val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
     3.1 --- a/src/Pure/context.ML	Mon Jan 04 22:43:07 2010 +0100
     3.2 +++ b/src/Pure/context.ML	Mon Jan 04 23:20:35 2010 +0100
     3.3 @@ -574,7 +574,7 @@
     3.4  
     3.5  (** theory data **)
     3.6  
     3.7 -signature OLD_THEORY_DATA_ARGS =
     3.8 +signature THEORY_DATA_PP_ARGS =
     3.9  sig
    3.10    type T
    3.11    val empty: T
    3.12 @@ -582,6 +582,14 @@
    3.13    val merge: Pretty.pp -> T * T -> T
    3.14  end;
    3.15  
    3.16 +signature THEORY_DATA_ARGS =
    3.17 +sig
    3.18 +  type T
    3.19 +  val empty: T
    3.20 +  val extend: T -> T
    3.21 +  val merge: T * T -> T
    3.22 +end;
    3.23 +
    3.24  signature THEORY_DATA =
    3.25  sig
    3.26    type T
    3.27 @@ -590,7 +598,7 @@
    3.28    val map: (T -> T) -> theory -> theory
    3.29  end;
    3.30  
    3.31 -functor TheoryDataFun(Data: OLD_THEORY_DATA_ARGS): THEORY_DATA =
    3.32 +functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA =
    3.33  struct
    3.34  
    3.35  type T = Data.T;
    3.36 @@ -607,28 +615,14 @@
    3.37  
    3.38  end;
    3.39  
    3.40 -signature THEORY_DATA_ARGS =
    3.41 -sig
    3.42 -  type T
    3.43 -  val empty: T
    3.44 -  val extend: T -> T
    3.45 -  val merge: T * T -> T
    3.46 -end;
    3.47 -
    3.48  functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
    3.49 -struct
    3.50 -
    3.51 -structure Result = TheoryDataFun
    3.52 -(
    3.53 -  type T = Data.T;
    3.54 -  val empty = Data.empty;
    3.55 -  val extend = Data.extend;
    3.56 -  fun merge _ = Data.merge;
    3.57 -);
    3.58 -
    3.59 -open Result;
    3.60 -
    3.61 -end;
    3.62 +  Theory_Data_PP
    3.63 +  (
    3.64 +    type T = Data.T;
    3.65 +    val empty = Data.empty;
    3.66 +    val extend = Data.extend;
    3.67 +    fun merge _ = Data.merge;
    3.68 +  );
    3.69  
    3.70  
    3.71  
     4.1 --- a/src/Pure/sign.ML	Mon Jan 04 22:43:07 2010 +0100
     4.2 +++ b/src/Pure/sign.ML	Mon Jan 04 23:20:35 2010 +0100
     4.3 @@ -148,7 +148,7 @@
     4.4  fun make_sign (naming, syn, tsig, consts) =
     4.5    Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
     4.6  
     4.7 -structure SignData = TheoryDataFun
     4.8 +structure SignData = Theory_Data_PP
     4.9  (
    4.10    type T = sign;
    4.11    fun extend (Sign {syn, tsig, consts, ...}) =
     5.1 --- a/src/Pure/theory.ML	Mon Jan 04 22:43:07 2010 +0100
     5.2 +++ b/src/Pure/theory.ML	Mon Jan 04 23:20:35 2010 +0100
     5.3 @@ -86,7 +86,7 @@
     5.4  
     5.5  fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
     5.6  
     5.7 -structure ThyData = TheoryDataFun
     5.8 +structure ThyData = Theory_Data_PP
     5.9  (
    5.10    type T = thy;
    5.11    val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;