1.1 --- a/src/Pure/Isar/attrib.ML	Fri Nov 09 00:18:23 2001 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Nov 09 00:19:20 2001 +0100
     1.3 @@ -56,6 +56,7 @@
     1.4  
     1.5    val empty = {space = NameSpace.empty, attrs = Symtab.empty};
     1.6    val copy = I;
     1.7 +  val finish = I;
     1.8    val prep_ext = I;
     1.9  
    1.10    fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) =

     2.1 --- a/src/Pure/Isar/calculation.ML	Fri Nov 09 00:18:23 2001 +0100
     2.2 +++ b/src/Pure/Isar/calculation.ML	Fri Nov 09 00:19:20 2001 +0100
     2.3 @@ -40,6 +40,7 @@
     2.4  
     2.5    val empty = NetRules.elim;
     2.6    val copy = I;
     2.7 +  val finish = I;
     2.8    val prep_ext = I;
     2.9    val merge = NetRules.merge;
    2.10    val print = print_rules Display.pretty_thm_sg;

     3.1 --- a/src/Pure/Isar/induct_attrib.ML	Fri Nov 09 00:18:23 2001 +0100
     3.2 +++ b/src/Pure/Isar/induct_attrib.ML	Fri Nov 09 00:19:20 2001 +0100
     3.3 @@ -110,6 +110,7 @@
     3.4      ((init_rules (first_var o #2), init_rules (Thm.major_prem_of o #2)),
     3.5       (init_rules (last_var o #2), init_rules (Thm.major_prem_of o #2)));
     3.6    val copy = I;
     3.7 +  val finish = I;
     3.8    val prep_ext = I;
     3.9    fun merge (((casesT1, casesS1), (inductT1, inductS1)),
    3.10        ((casesT2, casesS2), (inductT2, inductS2))) =

     4.1 --- a/src/Pure/Isar/object_logic.ML	Fri Nov 09 00:18:23 2001 +0100
     4.2 +++ b/src/Pure/Isar/object_logic.ML	Fri Nov 09 00:19:20 2001 +0100
     4.3 @@ -40,6 +40,7 @@
     4.4  
     4.5    val empty = (None, ([], [Drule.norm_hhf_eq]));
     4.6    val copy = I;
     4.7 +  val finish = I;
     4.8    val prep_ext = I;
     4.9  
    4.10    fun merge_judgment (Some x, Some y) =

     5.1 --- a/src/Pure/Isar/proof_context.ML	Fri Nov 09 00:18:23 2001 +0100
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Nov 09 00:19:20 2001 +0100
     5.3 @@ -212,6 +212,7 @@
     5.4  
     5.5    val empty = Symtab.empty;
     5.6    val copy = I;
     5.7 +  val finish = I;
     5.8    val prep_ext = I;
     5.9    fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
    5.10      handle Symtab.DUPS kinds => err_inconsistent kinds;

     6.1 --- a/src/Pure/Thy/present.ML	Fri Nov 09 00:18:23 2001 +0100
     6.2 +++ b/src/Pure/Thy/present.ML	Fri Nov 09 00:19:20 2001 +0100
     6.3 @@ -78,6 +78,7 @@
     6.4  
     6.5    val empty = {name = "Pure", session = [], is_local = false};
     6.6    val copy = I;
     6.7 +  val finish = I;
     6.8    fun prep_ext _ = {name = "", session = [], is_local = false};
     6.9    fun merge _ = empty;
    6.10    fun print _ _ = ();

     7.1 --- a/src/Pure/axclass.ML	Fri Nov 09 00:18:23 2001 +0100
     7.2 +++ b/src/Pure/axclass.ML	Fri Nov 09 00:19:20 2001 +0100
     7.3 @@ -172,6 +172,7 @@
     7.4  
     7.5    val empty = Symtab.empty;
     7.6    val copy = I;
     7.7 +  val finish = I;
     7.8    val prep_ext = I;
     7.9    fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2);
    7.10  

     8.1 --- a/src/Pure/codegen.ML	Fri Nov 09 00:18:23 2001 +0100
     8.2 +++ b/src/Pure/codegen.ML	Fri Nov 09 00:19:20 2001 +0100
     8.3 @@ -82,6 +82,7 @@
     8.4  
     8.5    val empty = {codegens = [], consts = [], types = []};
     8.6    val copy = I;
     8.7 +  val finish = I;
     8.8    val prep_ext = I;
     8.9  
    8.10    fun merge ({codegens = codegens1, consts = consts1, types = types1},

     9.1 --- a/src/Pure/goals.ML	Fri Nov 09 00:18:23 2001 +0100
     9.2 +++ b/src/Pure/goals.ML	Fri Nov 09 00:19:20 2001 +0100
     9.3 @@ -192,6 +192,7 @@
     9.4  
     9.5    val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
     9.6    fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs);
     9.7 +  val finish = I;
     9.8    fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []);
     9.9    fun merge ({space = space1, locales = locales1, scope = _},
    9.10      {space = space2, locales = locales2, scope = _}) =

    10.1 --- a/src/Pure/proofterm.ML	Fri Nov 09 00:18:23 2001 +0100
    10.2 +++ b/src/Pure/proofterm.ML	Fri Nov 09 00:19:20 2001 +0100
    10.3 @@ -1002,6 +1002,7 @@
    10.4  
    10.5    val empty = (ref ([], [])): T;
    10.6    fun copy (ref rews) = (ref rews): T;            (*create new reference!*)
    10.7 +  val finish = I;
    10.8    val prep_ext = copy;
    10.9    fun merge (ref (rules1, procs1), ref (rules2, procs2)) = ref
   10.10      (merge_lists rules1 rules2,

    11.1 --- a/src/Pure/pure_thy.ML	Fri Nov 09 00:18:23 2001 +0100
    11.2 +++ b/src/Pure/pure_thy.ML	Fri Nov 09 00:19:20 2001 +0100
    11.3 @@ -83,6 +83,7 @@
    11.4  
    11.5    val empty = mk_empty ();
    11.6    fun copy (ref x) = ref x;
    11.7 +  val finish = I;
    11.8    val prep_ext = mk_empty;
    11.9    val merge = mk_empty;
   11.10  
   11.11 @@ -386,6 +387,7 @@
   11.12  
   11.13    val empty = {name = "", version = 0};
   11.14    val copy = I;
   11.15 +  val finish = I;
   11.16    val prep_ext  = I;
   11.17    fun merge _ = empty;
   11.18    fun print _ _ = ();
   11.19 @@ -417,7 +419,10 @@
   11.20    |> put_name name
   11.21    |> local_path;
   11.22  
   11.23 -fun end_theory thy = Theory.add_name (get_name thy) thy;
   11.24 +fun end_theory thy =
   11.25 +  thy
   11.26 +  |> Theory.finish
   11.27 +  |> Theory.add_name (get_name thy);
   11.28  
   11.29  fun checkpoint thy =
   11.30    if is_draft thy then
   11.31 @@ -473,7 +478,6 @@
   11.32      ("itself", [logicS], logicS)]
   11.33    |> Theory.add_nonterminals Syntax.pure_nonterms
   11.34    |> Theory.add_syntax Syntax.pure_syntax
   11.35 -  |> Theory.add_modesyntax (Symbol.symbolsN, true) Syntax.pure_sym_syntax
   11.36    |> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
   11.37    |> Theory.add_trfuns Syntax.pure_trfuns
   11.38    |> Theory.add_trfunsT Syntax.pure_trfunsT

    12.1 --- a/src/Pure/sign.ML	Fri Nov 09 00:18:23 2001 +0100
    12.2 +++ b/src/Pure/sign.ML	Fri Nov 09 00:19:20 2001 +0100
    12.3 @@ -148,8 +148,9 @@
    12.4    val data_kinds: data -> string list
    12.5    val merge_refs: sg_ref * sg_ref -> sg_ref
    12.6    val merge: sg * sg -> sg
    12.7 +  val copy: sg -> sg
    12.8 +  val finish: sg -> sg
    12.9    val prep_ext: sg -> sg
   12.10 -  val copy: sg -> sg
   12.11    val PureN: string
   12.12    val CPureN: string
   12.13    val nontriv_merge: sg * sg -> sg
   12.14 @@ -162,7 +163,8 @@
   12.15  sig
   12.16    include SIGN
   12.17    val init_data: Object.kind * (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
   12.18 -    (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
   12.19 +    (Object.T -> Object.T) * (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit))
   12.20 +    -> sg -> sg
   12.21    val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
   12.22    val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
   12.23    val print_data: Object.kind -> sg -> unit
   12.24 @@ -191,8 +193,9 @@
   12.25    Data of
   12.26      (Object.kind *                              (*kind (for authorization)*)
   12.27        (Object.T *                               (*value*)
   12.28 -        ((Object.T -> Object.T) *               (*prepare extend method*)
   12.29 -          (Object.T -> Object.T) *              (*copy method*)
   12.30 +        ((Object.T -> Object.T) *               (*copy method*)
   12.31 +          (Object.T -> Object.T) *              (*finish method*)
   12.32 +          (Object.T -> Object.T) *              (*prepare extend method*)
   12.33            (Object.T * Object.T -> Object.T) *   (*merge and prepare extend method*)
   12.34            (sg -> Object.T -> unit))))           (*print method*)
   12.35      Symtab.table
   12.36 @@ -337,9 +340,9 @@
   12.37         None => []
   12.38       | Some x => [(kind, x)]);
   12.39  
   12.40 -    fun merge_entries [(kind, (e, mths as (_, ext, _, _)))] =
   12.41 +    fun merge_entries [(kind, (e, mths as (_, _, ext, _, _)))] =
   12.42            (kind, (ext e handle exn => err_method "prep_ext" (Object.name_of_kind kind) exn, mths))
   12.43 -      | merge_entries [(kind, (e1, mths as (_, _, mrg, _))), (_, (e2, _))] =
   12.44 +      | merge_entries [(kind, (e1, mths as (_, _, _, mrg, _))), (_, (e2, _))] =
   12.45            (kind, (mrg (e1, e2)
   12.46              handle exn => err_method "merge" (Object.name_of_kind kind) exn, mths))
   12.47        | merge_entries _ = sys_error "merge_entries";
   12.48 @@ -353,9 +356,9 @@
   12.49  
   12.50  fun prep_ext_data data = merge_data (data, empty_data);
   12.51  
   12.52 -fun init_data_sg sg (Data tab) kind e cp ext mrg prt =
   12.53 +fun init_data_sg sg (Data tab) kind e cp fin ext mrg prt =
   12.54    let val name = Object.name_of_kind kind in
   12.55 -    Data (Symtab.update_new ((name, (kind, (e, (cp, ext, mrg, prt)))), tab))
   12.56 +    Data (Symtab.update_new ((name, (kind, (e, (cp, fin, ext, mrg, prt)))), tab))
   12.57        handle Symtab.DUP _ => err_dup_init sg name
   12.58    end;
   12.59  
   12.60 @@ -378,7 +381,7 @@
   12.61    in f x handle Match => Object.kind_error kind end;
   12.62  
   12.63  fun print_data kind (sg as Sg (_, {data = Data tab, ...})) =
   12.64 -  let val (e, (_, _, _, prt)) = lookup_data sg tab kind
   12.65 +  let val (e, (_, _, _, _, prt)) = lookup_data sg tab kind
   12.66    in prt sg e handle exn => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) exn end;
   12.67  
   12.68  fun put_data_sg sg (Data tab) kind f x =
   12.69 @@ -1015,14 +1018,21 @@
   12.70  
   12.71  (* signature data *)
   12.72  
   12.73 -fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, ext, mrg, prt)) =
   12.74 -  (syn, tsig, ctab, names, init_data_sg sg data kind e cp ext mrg prt);
   12.75 +fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, fin, ext, mrg, prt)) =
   12.76 +  (syn, tsig, ctab, names, init_data_sg sg data kind e cp fin ext mrg prt);
   12.77  
   12.78  fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, f, x) =
   12.79    (syn, tsig, ctab, names, put_data_sg sg data kind f x);
   12.80  
   12.81  
   12.82 -fun copy_data (k, (e, mths as (cp, _, _, _))) =
   12.83 +fun finish_data (k, (e, mths as (_, fin, _, _, _))) =
   12.84 +  (k, (fin e handle exn => err_method "finish" (Object.name_of_kind k) exn, mths));
   12.85 +
   12.86 +fun ext_finish_data (syn, tsig, ctab, names, Data tab) () =
   12.87 +  (syn, tsig, ctab, names, Data (Symtab.map finish_data tab));
   12.88 +
   12.89 +
   12.90 +fun copy_data (k, (e, mths as (cp, _, _, _, _))) =
   12.91    (k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths));
   12.92  
   12.93  fun copy (sg as Sg ({id = _, stamps}, {self, tsig, const_tab, syn, path, spaces, data})) =
   12.94 @@ -1065,6 +1075,7 @@
   12.95  val hide_space_i      = extend_sign true ext_hide_space_i "#";
   12.96  fun init_data arg sg  = extend_sign true (ext_init_data sg) "#" arg sg;
   12.97  fun put_data k f x sg = extend_sign true (ext_put_data sg) "#" (k, f, x) sg;
   12.98 +fun finish sg         = extend_sign true ext_finish_data "#" () sg;
   12.99  fun add_name name sg  = extend_sign true K name () sg;
  12.100  fun prep_ext sg       = extend_sign false K "#" () sg;
  12.101  

    13.1 --- a/src/Pure/theory.ML	Fri Nov 09 00:18:23 2001 +0100
    13.2 +++ b/src/Pure/theory.ML	Fri Nov 09 00:19:20 2001 +0100
    13.3 @@ -86,6 +86,7 @@
    13.4    val hide_consts: string list -> theory -> theory
    13.5    val add_name: string -> theory -> theory
    13.6    val copy: theory -> theory
    13.7 +  val finish: theory -> theory
    13.8    val prep_ext: theory -> theory
    13.9    val prep_ext_merge: theory list -> theory
   13.10    val requires: theory -> string -> string -> unit
   13.11 @@ -97,7 +98,8 @@
   13.12  sig
   13.13    include THEORY
   13.14    val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
   13.15 -    (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
   13.16 +    (Object.T -> Object.T) * (Object.T * Object.T -> Object.T) *
   13.17 +    (Sign.sg -> Object.T -> unit)) -> theory -> theory
   13.18    val print_data: Object.kind -> theory -> unit
   13.19    val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
   13.20    val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
   13.21 @@ -227,6 +229,7 @@
   13.22  val hide_consts      = curry hide_space_i Sign.constK;
   13.23  val add_name         = ext_sign Sign.add_name;
   13.24  val copy             = ext_sign (K Sign.copy) ();
   13.25 +val finish           = ext_sign (K Sign.finish) ();
   13.26  val prep_ext         = ext_sign (K Sign.prep_ext) ();
   13.27  
   13.28  

    14.1 --- a/src/Pure/theory_data.ML	Fri Nov 09 00:18:23 2001 +0100
    14.2 +++ b/src/Pure/theory_data.ML	Fri Nov 09 00:19:20 2001 +0100
    14.3 @@ -11,6 +11,7 @@
    14.4    type T
    14.5    val empty: T
    14.6    val copy: T -> T
    14.7 +  val finish: T -> T
    14.8    val prep_ext: T -> T
    14.9    val merge: T * T -> T
   14.10    val print: Sign.sg -> T -> unit
   14.11 @@ -40,6 +41,7 @@
   14.12    Theory.init_data kind
   14.13      (Data Args.empty,
   14.14        fn (Data x) => Data (Args.copy x),
   14.15 +      fn (Data x) => Data (Args.finish x),
   14.16        fn (Data x) => Data (Args.prep_ext x),
   14.17        fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
   14.18        fn sg => fn (Data x) => Args.print sg x);

    15.1 --- a/src/Sequents/prover.ML	Fri Nov 09 00:18:23 2001 +0100
    15.2 +++ b/src/Sequents/prover.ML	Fri Nov 09 00:19:20 2001 +0100
    15.3 @@ -174,6 +174,7 @@
    15.4    type T = pack ref;
    15.5    val empty = ref empty_pack
    15.6    fun copy (ref pack) = ref pack;
    15.7 +  val finish = I;
    15.8    val prep_ext = copy;
    15.9    fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
   15.10    fun print _ (ref pack) = print_pack pack;