theory data: copy;

--- a/src/Pure/Isar/attrib.ML	Fri Apr 30 17:59:36 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Apr 30 18:01:11 1999 +0200
@@ -50,6 +50,7 @@
          * string) * stamp) Symtab.table};
 
   val empty = {space = NameSpace.empty, attrs = Symtab.empty};
+  val copy = I;
   val prep_ext = I;
 
   fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) =

--- a/src/Pure/Isar/method.ML	Fri Apr 30 17:59:36 1999 +0200
+++ b/src/Pure/Isar/method.ML	Fri Apr 30 18:01:11 1999 +0200
@@ -146,6 +146,7 @@
      meths: (((Args.src -> Proof.context -> Proof.method) * string) * stamp) Symtab.table};
 
   val empty = {space = NameSpace.empty, meths = Symtab.empty};
+  val copy = I;
   val prep_ext = I;
   fun merge ({space = space1, meths = meths1}, {space = space2, meths = meths2}) =
     {space = NameSpace.merge (space1, space2),

--- a/src/Pure/axclass.ML	Fri Apr 30 17:59:36 1999 +0200
+++ b/src/Pure/axclass.ML	Fri Apr 30 18:01:11 1999 +0200
@@ -174,6 +174,7 @@
   type T = axclass_info Symtab.table;
 
   val empty = Symtab.empty;
+  val copy = I;
   val prep_ext = I;
   fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2);
 

--- a/src/Pure/locale.ML	Fri Apr 30 17:59:36 1999 +0200
+++ b/src/Pure/locale.ML	Fri Apr 30 18:01:11 1999 +0200
@@ -112,6 +112,7 @@
   type T = locale_data;
 
   val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
+  fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs);
   fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []);
   fun merge ({space = space1, locales = locales1, scope = _},
     {space = space2, locales = locales2, scope = _}) =

--- a/src/Pure/sign.ML	Fri Apr 30 17:59:36 1999 +0200
+++ b/src/Pure/sign.ML	Fri Apr 30 18:01:11 1999 +0200
@@ -124,6 +124,7 @@
   val merge_refs: sg_ref * sg_ref -> sg_ref
   val merge: sg * sg -> sg
   val prep_ext: sg -> sg
+  val copy: sg -> sg
   val nontriv_merge: sg * sg -> sg
   val pre_pure: sg
   val const_of_class: class -> string
@@ -133,7 +134,7 @@
 signature PRIVATE_SIGN =
 sig
   include SIGN
-  val init_data: Object.kind * (Object.T * (Object.T -> Object.T) *
+  val init_data: Object.kind * (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
     (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
   val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
   val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
@@ -164,6 +165,7 @@
     (Object.kind *				(*kind (for authorization)*)
       (Object.T *				(*value*)
         ((Object.T -> Object.T) *               (*prepare extend method*)
+          (Object.T -> Object.T) *              (*copy method*)
           (Object.T * Object.T -> Object.T) *   (*merge and prepare extend method*)
           (sg -> Object.T -> unit))))           (*print method*)
     Symtab.table
@@ -306,9 +308,9 @@
        None => []
      | Some x => [(kind, x)]);
 
-    fun merge_entries [(kind, (e, mths as (ext, _, _)))] =
+    fun merge_entries [(kind, (e, mths as (_, ext, _, _)))] =
           (kind, (ext e handle _ => err_method "prep_ext" (Object.name_of_kind kind), mths))
-      | merge_entries [(kind, (e1, mths as (_, mrg, _))), (_, (e2, _))] =
+      | merge_entries [(kind, (e1, mths as (_, _, mrg, _))), (_, (e2, _))] =
           (kind, (mrg (e1, e2) handle _ => err_method "merge" (Object.name_of_kind kind), mths))
       | merge_entries _ = sys_error "merge_entries";
 
@@ -321,9 +323,9 @@
 
 fun prep_ext_data data = merge_data (data, empty_data);
 
-fun init_data_sg sg (Data tab) kind e ext mrg prt =
+fun init_data_sg sg (Data tab) kind e cp ext mrg prt =
   let val name = Object.name_of_kind kind in
-    Data (Symtab.update_new ((name, (kind, (e, (ext, mrg, prt)))), tab))
+    Data (Symtab.update_new ((name, (kind, (e, (cp, ext, mrg, prt)))), tab))
       handle Symtab.DUP _ => err_dup_init sg name
   end;
 
@@ -346,7 +348,7 @@
   in f x handle Match => Object.kind_error kind end;
 
 fun print_data kind (sg as Sg (_, {data = Data tab, ...})) =
-  let val (e, (_, _, prt)) = lookup_data sg tab kind
+  let val (e, (_, _, _, prt)) = lookup_data sg tab kind
   in prt sg e handle _ => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) end;
 
 fun put_data_sg sg (Data tab) kind f x =
@@ -903,13 +905,25 @@
 
 (* signature data *)
 
-fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, ext, mrg, prt)) =
-  (syn, tsig, ctab, names, init_data_sg sg data kind e ext mrg prt);
+fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, ext, mrg, prt)) =
+  (syn, tsig, ctab, names, init_data_sg sg data kind e cp ext mrg prt);
 
 fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, f, x) =
   (syn, tsig, ctab, names, put_data_sg sg data kind f x);
 
 
+fun copy_data (k, (e, mths as (cp, _, _, _))) =
+  (k, (cp e handle _ => err_method "copy" (Object.name_of_kind k), mths));
+
+fun copy (sg as Sg ({id = _, stamps}, {self, tsig, const_tab, syn, path, spaces, data})) =
+  let
+    val _ = check_stale sg;
+    val self' = SgRef (Some (ref sg));
+    val Data tab = data;
+    val data' = Data (Symtab.map copy_data tab);
+  in create_sign self' stamps "#" (syn, tsig, const_tab, (path, spaces), data') end;
+
+
 (* the external interfaces *)
 
 val add_classes       = extend_sign true (ext_classes true) "#";

--- a/src/Pure/theory.ML	Fri Apr 30 17:59:36 1999 +0200
+++ b/src/Pure/theory.ML	Fri Apr 30 18:01:11 1999 +0200
@@ -91,7 +91,7 @@
 signature PRIVATE_THEORY =
 sig
   include THEORY
-  val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) *
+  val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
     (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
   val print_data: Object.kind -> theory -> unit
   val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
@@ -212,7 +212,7 @@
 val add_space        = ext_sign Sign.add_space;
 val add_name         = ext_sign Sign.add_name;
 val prep_ext         = ext_sign (K Sign.prep_ext) ();
-val copy             = prep_ext;	(*an approximation ...*)
+val copy             = ext_sign (K Sign.copy) ();
 
 
 

--- a/src/Pure/theory_data.ML	Fri Apr 30 17:59:36 1999 +0200
+++ b/src/Pure/theory_data.ML	Fri Apr 30 18:01:11 1999 +0200
@@ -10,6 +10,7 @@
   val name: string
   type T
   val empty: T
+  val copy: T -> T
   val prep_ext: T -> T
   val merge: T * T -> T
   val print: Sign.sg -> T -> unit
@@ -37,6 +38,7 @@
 val init =
   Theory.init_data kind
     (Data Args.empty,
+      fn (Data x) => Data (Args.copy x),
       fn (Data x) => Data (Args.prep_ext x),
       fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
       fn sg => fn (Data x) => Args.print sg x);