src/Pure/sign.ML
changeset 6546 995a66249a9b
parent 6311 15652e058e28
child 6845 598d2f32d452
     1.1 --- a/src/Pure/sign.ML	Fri Apr 30 17:59:36 1999 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Apr 30 18:01:11 1999 +0200
     1.3 @@ -124,6 +124,7 @@
     1.4    val merge_refs: sg_ref * sg_ref -> sg_ref
     1.5    val merge: sg * sg -> sg
     1.6    val prep_ext: sg -> sg
     1.7 +  val copy: sg -> sg
     1.8    val nontriv_merge: sg * sg -> sg
     1.9    val pre_pure: sg
    1.10    val const_of_class: class -> string
    1.11 @@ -133,7 +134,7 @@
    1.12  signature PRIVATE_SIGN =
    1.13  sig
    1.14    include SIGN
    1.15 -  val init_data: Object.kind * (Object.T * (Object.T -> Object.T) *
    1.16 +  val init_data: Object.kind * (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
    1.17      (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
    1.18    val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
    1.19    val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
    1.20 @@ -164,6 +165,7 @@
    1.21      (Object.kind *				(*kind (for authorization)*)
    1.22        (Object.T *				(*value*)
    1.23          ((Object.T -> Object.T) *               (*prepare extend method*)
    1.24 +          (Object.T -> Object.T) *              (*copy method*)
    1.25            (Object.T * Object.T -> Object.T) *   (*merge and prepare extend method*)
    1.26            (sg -> Object.T -> unit))))           (*print method*)
    1.27      Symtab.table
    1.28 @@ -306,9 +308,9 @@
    1.29         None => []
    1.30       | Some x => [(kind, x)]);
    1.31  
    1.32 -    fun merge_entries [(kind, (e, mths as (ext, _, _)))] =
    1.33 +    fun merge_entries [(kind, (e, mths as (_, ext, _, _)))] =
    1.34            (kind, (ext e handle _ => err_method "prep_ext" (Object.name_of_kind kind), mths))
    1.35 -      | merge_entries [(kind, (e1, mths as (_, mrg, _))), (_, (e2, _))] =
    1.36 +      | merge_entries [(kind, (e1, mths as (_, _, mrg, _))), (_, (e2, _))] =
    1.37            (kind, (mrg (e1, e2) handle _ => err_method "merge" (Object.name_of_kind kind), mths))
    1.38        | merge_entries _ = sys_error "merge_entries";
    1.39  
    1.40 @@ -321,9 +323,9 @@
    1.41  
    1.42  fun prep_ext_data data = merge_data (data, empty_data);
    1.43  
    1.44 -fun init_data_sg sg (Data tab) kind e ext mrg prt =
    1.45 +fun init_data_sg sg (Data tab) kind e cp ext mrg prt =
    1.46    let val name = Object.name_of_kind kind in
    1.47 -    Data (Symtab.update_new ((name, (kind, (e, (ext, mrg, prt)))), tab))
    1.48 +    Data (Symtab.update_new ((name, (kind, (e, (cp, ext, mrg, prt)))), tab))
    1.49        handle Symtab.DUP _ => err_dup_init sg name
    1.50    end;
    1.51  
    1.52 @@ -346,7 +348,7 @@
    1.53    in f x handle Match => Object.kind_error kind end;
    1.54  
    1.55  fun print_data kind (sg as Sg (_, {data = Data tab, ...})) =
    1.56 -  let val (e, (_, _, prt)) = lookup_data sg tab kind
    1.57 +  let val (e, (_, _, _, prt)) = lookup_data sg tab kind
    1.58    in prt sg e handle _ => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) end;
    1.59  
    1.60  fun put_data_sg sg (Data tab) kind f x =
    1.61 @@ -903,13 +905,25 @@
    1.62  
    1.63  (* signature data *)
    1.64  
    1.65 -fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, ext, mrg, prt)) =
    1.66 -  (syn, tsig, ctab, names, init_data_sg sg data kind e ext mrg prt);
    1.67 +fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, ext, mrg, prt)) =
    1.68 +  (syn, tsig, ctab, names, init_data_sg sg data kind e cp ext mrg prt);
    1.69  
    1.70  fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, f, x) =
    1.71    (syn, tsig, ctab, names, put_data_sg sg data kind f x);
    1.72  
    1.73  
    1.74 +fun copy_data (k, (e, mths as (cp, _, _, _))) =
    1.75 +  (k, (cp e handle _ => err_method "copy" (Object.name_of_kind k), mths));
    1.76 +
    1.77 +fun copy (sg as Sg ({id = _, stamps}, {self, tsig, const_tab, syn, path, spaces, data})) =
    1.78 +  let
    1.79 +    val _ = check_stale sg;
    1.80 +    val self' = SgRef (Some (ref sg));
    1.81 +    val Data tab = data;
    1.82 +    val data' = Data (Symtab.map copy_data tab);
    1.83 +  in create_sign self' stamps "#" (syn, tsig, const_tab, (path, spaces), data') end;
    1.84 +
    1.85 +
    1.86  (* the external interfaces *)
    1.87  
    1.88  val add_classes       = extend_sign true (ext_classes true) "#";