src/Pure/context.ML
changeset 34245 25bd3ed2ac9f
parent 33606 2b27020ffcb2
child 34253 5930c6391126
     1.1 --- a/src/Pure/context.ML	Mon Jan 04 14:09:56 2010 +0100
     1.2 +++ b/src/Pure/context.ML	Mon Jan 04 14:09:56 2010 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4    include CONTEXT
     1.5    structure Theory_Data:
     1.6    sig
     1.7 -    val declare: Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) ->
     1.8 +    val declare: Object.T -> (Object.T -> Object.T) ->
     1.9        (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
    1.10      val get: serial -> (Object.T -> 'a) -> theory -> 'a
    1.11      val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
    1.12 @@ -112,7 +112,6 @@
    1.13  
    1.14  type kind =
    1.15   {empty: Object.T,
    1.16 -  copy: Object.T -> Object.T,
    1.17    extend: Object.T -> Object.T,
    1.18    merge: Pretty.pp -> Object.T * Object.T -> Object.T};
    1.19  
    1.20 @@ -126,18 +125,16 @@
    1.21  in
    1.22  
    1.23  fun invoke_empty k = invoke (K o #empty) k ();
    1.24 -val invoke_copy = invoke #copy;
    1.25  val invoke_extend = invoke #extend;
    1.26  fun invoke_merge pp = invoke (fn kind => #merge kind pp);
    1.27  
    1.28 -fun declare_theory_data empty copy extend merge =
    1.29 +fun declare_theory_data empty extend merge =
    1.30    let
    1.31      val k = serial ();
    1.32 -    val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
    1.33 +    val kind = {empty = empty, extend = extend, merge = merge};
    1.34      val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
    1.35    in k end;
    1.36  
    1.37 -val copy_data = Datatab.map' invoke_copy;
    1.38  val extend_data = Datatab.map' invoke_extend;
    1.39  
    1.40  fun merge_data pp (data1, data2) =
    1.41 @@ -341,7 +338,7 @@
    1.42      val (self', data', ancestry') =
    1.43        if draft then (self, data, ancestry)    (*destructive change!*)
    1.44        else if #stage history > 0
    1.45 -      then (NONE, copy_data data, ancestry)
    1.46 +      then (NONE, data, ancestry)
    1.47        else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors_of thy));
    1.48      val ids' = insert_id draft id ids;
    1.49      val data'' = f data';
    1.50 @@ -357,9 +354,8 @@
    1.51    let
    1.52      val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy;
    1.53      val ids' = insert_id draft id ids;
    1.54 -    val data' = copy_data data;
    1.55      val thy' = SYNCHRONIZED (fn () =>
    1.56 -      (check_thy thy; create_thy NONE true ids' data' ancestry history));
    1.57 +      (check_thy thy; create_thy NONE true ids' data ancestry history));
    1.58    in thy' end;
    1.59  
    1.60  val pre_pure_thy = create_thy NONE true Inttab.empty
    1.61 @@ -430,9 +426,9 @@
    1.62  val declare = declare_theory_data;
    1.63  
    1.64  fun get k dest thy =
    1.65 -  dest ((case Datatab.lookup (data_of thy) k of
    1.66 +  dest (case Datatab.lookup (data_of thy) k of
    1.67      SOME x => x
    1.68 -  | NONE => invoke_copy k (invoke_empty k)));   (*adhoc value*)
    1.69 +  | NONE => invoke_empty k);   (*adhoc value*)
    1.70  
    1.71  fun put k mk x = modify_thy (Datatab.update (k, mk x));
    1.72  
    1.73 @@ -582,7 +578,6 @@
    1.74  sig
    1.75    type T
    1.76    val empty: T
    1.77 -  val copy: T -> T
    1.78    val extend: T -> T
    1.79    val merge: Pretty.pp -> T * T -> T
    1.80  end;
    1.81 @@ -604,7 +599,6 @@
    1.82  
    1.83  val kind = Context.Theory_Data.declare
    1.84    (Data Data.empty)
    1.85 -  (fn Data x => Data (Data.copy x))
    1.86    (fn Data x => Data (Data.extend x))
    1.87    (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
    1.88  
    1.89 @@ -639,7 +633,6 @@
    1.90  (
    1.91    type T = Data.T;
    1.92    val empty = Data.empty;
    1.93 -  val copy = I;
    1.94    val extend = Data.extend;
    1.95    fun merge _ = Data.merge;
    1.96  );