dropped copy operation for legacy TheoryDataFun
authorhaftmann
Mon Jan 04 14:09:56 2010 +0100 (2010-01-04 ago)
changeset 3424525bd3ed2ac9f
parent 34244 03f8dcab55f3
child 34246 5eaff81220a9
dropped copy operation for legacy TheoryDataFun
src/Pure/axclass.ML
src/Pure/context.ML
src/Pure/sign.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/axclass.ML	Mon Jan 04 14:09:56 2010 +0100
     1.2 +++ b/src/Pure/axclass.ML	Mon Jan 04 14:09:56 2010 +0100
     1.3 @@ -118,7 +118,6 @@
     1.4  (
     1.5    type T = axclasses * (instances * inst_params);
     1.6    val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
     1.7 -  val copy = I;
     1.8    val extend = I;
     1.9    fun merge pp ((axclasses1, (instances1, inst_params1)), (axclasses2, (instances2, inst_params2))) =
    1.10      (merge_axclasses pp (axclasses1, axclasses2),
     2.1 --- a/src/Pure/context.ML	Mon Jan 04 14:09:56 2010 +0100
     2.2 +++ b/src/Pure/context.ML	Mon Jan 04 14:09:56 2010 +0100
     2.3 @@ -83,7 +83,7 @@
     2.4    include CONTEXT
     2.5    structure Theory_Data:
     2.6    sig
     2.7 -    val declare: Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) ->
     2.8 +    val declare: Object.T -> (Object.T -> Object.T) ->
     2.9        (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
    2.10      val get: serial -> (Object.T -> 'a) -> theory -> 'a
    2.11      val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
    2.12 @@ -112,7 +112,6 @@
    2.13  
    2.14  type kind =
    2.15   {empty: Object.T,
    2.16 -  copy: Object.T -> Object.T,
    2.17    extend: Object.T -> Object.T,
    2.18    merge: Pretty.pp -> Object.T * Object.T -> Object.T};
    2.19  
    2.20 @@ -126,18 +125,16 @@
    2.21  in
    2.22  
    2.23  fun invoke_empty k = invoke (K o #empty) k ();
    2.24 -val invoke_copy = invoke #copy;
    2.25  val invoke_extend = invoke #extend;
    2.26  fun invoke_merge pp = invoke (fn kind => #merge kind pp);
    2.27  
    2.28 -fun declare_theory_data empty copy extend merge =
    2.29 +fun declare_theory_data empty extend merge =
    2.30    let
    2.31      val k = serial ();
    2.32 -    val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
    2.33 +    val kind = {empty = empty, extend = extend, merge = merge};
    2.34      val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
    2.35    in k end;
    2.36  
    2.37 -val copy_data = Datatab.map' invoke_copy;
    2.38  val extend_data = Datatab.map' invoke_extend;
    2.39  
    2.40  fun merge_data pp (data1, data2) =
    2.41 @@ -341,7 +338,7 @@
    2.42      val (self', data', ancestry') =
    2.43        if draft then (self, data, ancestry)    (*destructive change!*)
    2.44        else if #stage history > 0
    2.45 -      then (NONE, copy_data data, ancestry)
    2.46 +      then (NONE, data, ancestry)
    2.47        else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors_of thy));
    2.48      val ids' = insert_id draft id ids;
    2.49      val data'' = f data';
    2.50 @@ -357,9 +354,8 @@
    2.51    let
    2.52      val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy;
    2.53      val ids' = insert_id draft id ids;
    2.54 -    val data' = copy_data data;
    2.55      val thy' = SYNCHRONIZED (fn () =>
    2.56 -      (check_thy thy; create_thy NONE true ids' data' ancestry history));
    2.57 +      (check_thy thy; create_thy NONE true ids' data ancestry history));
    2.58    in thy' end;
    2.59  
    2.60  val pre_pure_thy = create_thy NONE true Inttab.empty
    2.61 @@ -430,9 +426,9 @@
    2.62  val declare = declare_theory_data;
    2.63  
    2.64  fun get k dest thy =
    2.65 -  dest ((case Datatab.lookup (data_of thy) k of
    2.66 +  dest (case Datatab.lookup (data_of thy) k of
    2.67      SOME x => x
    2.68 -  | NONE => invoke_copy k (invoke_empty k)));   (*adhoc value*)
    2.69 +  | NONE => invoke_empty k);   (*adhoc value*)
    2.70  
    2.71  fun put k mk x = modify_thy (Datatab.update (k, mk x));
    2.72  
    2.73 @@ -582,7 +578,6 @@
    2.74  sig
    2.75    type T
    2.76    val empty: T
    2.77 -  val copy: T -> T
    2.78    val extend: T -> T
    2.79    val merge: Pretty.pp -> T * T -> T
    2.80  end;
    2.81 @@ -604,7 +599,6 @@
    2.82  
    2.83  val kind = Context.Theory_Data.declare
    2.84    (Data Data.empty)
    2.85 -  (fn Data x => Data (Data.copy x))
    2.86    (fn Data x => Data (Data.extend x))
    2.87    (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
    2.88  
    2.89 @@ -639,7 +633,6 @@
    2.90  (
    2.91    type T = Data.T;
    2.92    val empty = Data.empty;
    2.93 -  val copy = I;
    2.94    val extend = Data.extend;
    2.95    fun merge _ = Data.merge;
    2.96  );
     3.1 --- a/src/Pure/sign.ML	Mon Jan 04 14:09:56 2010 +0100
     3.2 +++ b/src/Pure/sign.ML	Mon Jan 04 14:09:56 2010 +0100
     3.3 @@ -151,7 +151,6 @@
     3.4  structure SignData = TheoryDataFun
     3.5  (
     3.6    type T = sign;
     3.7 -  val copy = I;
     3.8    fun extend (Sign {syn, tsig, consts, ...}) =
     3.9      make_sign (Name_Space.default_naming, syn, tsig, consts);
    3.10  
     4.1 --- a/src/Pure/theory.ML	Mon Jan 04 14:09:56 2010 +0100
     4.2 +++ b/src/Pure/theory.ML	Mon Jan 04 14:09:56 2010 +0100
     4.3 @@ -91,7 +91,6 @@
     4.4    type T = thy;
     4.5    val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
     4.6    val empty = make_thy (empty_axioms, Defs.empty, ([], []));
     4.7 -  val copy = I;
     4.8  
     4.9    fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);
    4.10