--- a/src/Pure/Isar/attrib.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/Isar/attrib.ML Fri Nov 09 00:19:20 2001 +0100
@@ -56,6 +56,7 @@
val empty = {space = NameSpace.empty, attrs = Symtab.empty};
val copy = I;
+ val finish = I;
val prep_ext = I;
fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) =
--- a/src/Pure/Isar/calculation.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/Isar/calculation.ML Fri Nov 09 00:19:20 2001 +0100
@@ -40,6 +40,7 @@
val empty = NetRules.elim;
val copy = I;
+ val finish = I;
val prep_ext = I;
val merge = NetRules.merge;
val print = print_rules Display.pretty_thm_sg;
--- a/src/Pure/Isar/induct_attrib.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/Isar/induct_attrib.ML Fri Nov 09 00:19:20 2001 +0100
@@ -110,6 +110,7 @@
((init_rules (first_var o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (last_var o #2), init_rules (Thm.major_prem_of o #2)));
val copy = I;
+ val finish = I;
val prep_ext = I;
fun merge (((casesT1, casesS1), (inductT1, inductS1)),
((casesT2, casesS2), (inductT2, inductS2))) =
--- a/src/Pure/Isar/object_logic.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/Isar/object_logic.ML Fri Nov 09 00:19:20 2001 +0100
@@ -40,6 +40,7 @@
val empty = (None, ([], [Drule.norm_hhf_eq]));
val copy = I;
+ val finish = I;
val prep_ext = I;
fun merge_judgment (Some x, Some y) =
--- a/src/Pure/Isar/proof_context.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Nov 09 00:19:20 2001 +0100
@@ -212,6 +212,7 @@
val empty = Symtab.empty;
val copy = I;
+ val finish = I;
val prep_ext = I;
fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
handle Symtab.DUPS kinds => err_inconsistent kinds;
--- a/src/Pure/Thy/present.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/Thy/present.ML Fri Nov 09 00:19:20 2001 +0100
@@ -78,6 +78,7 @@
val empty = {name = "Pure", session = [], is_local = false};
val copy = I;
+ val finish = I;
fun prep_ext _ = {name = "", session = [], is_local = false};
fun merge _ = empty;
fun print _ _ = ();
--- a/src/Pure/axclass.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/axclass.ML Fri Nov 09 00:19:20 2001 +0100
@@ -172,6 +172,7 @@
val empty = Symtab.empty;
val copy = I;
+ val finish = I;
val prep_ext = I;
fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2);
--- a/src/Pure/codegen.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/codegen.ML Fri Nov 09 00:19:20 2001 +0100
@@ -82,6 +82,7 @@
val empty = {codegens = [], consts = [], types = []};
val copy = I;
+ val finish = I;
val prep_ext = I;
fun merge ({codegens = codegens1, consts = consts1, types = types1},
--- a/src/Pure/goals.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/goals.ML Fri Nov 09 00:19:20 2001 +0100
@@ -192,6 +192,7 @@
val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs);
+ val finish = I;
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/proofterm.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/proofterm.ML Fri Nov 09 00:19:20 2001 +0100
@@ -1002,6 +1002,7 @@
val empty = (ref ([], [])): T;
fun copy (ref rews) = (ref rews): T; (*create new reference!*)
+ val finish = I;
val prep_ext = copy;
fun merge (ref (rules1, procs1), ref (rules2, procs2)) = ref
(merge_lists rules1 rules2,
--- a/src/Pure/pure_thy.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/pure_thy.ML Fri Nov 09 00:19:20 2001 +0100
@@ -83,6 +83,7 @@
val empty = mk_empty ();
fun copy (ref x) = ref x;
+ val finish = I;
val prep_ext = mk_empty;
val merge = mk_empty;
@@ -386,6 +387,7 @@
val empty = {name = "", version = 0};
val copy = I;
+ val finish = I;
val prep_ext = I;
fun merge _ = empty;
fun print _ _ = ();
@@ -417,7 +419,10 @@
|> put_name name
|> local_path;
-fun end_theory thy = Theory.add_name (get_name thy) thy;
+fun end_theory thy =
+ thy
+ |> Theory.finish
+ |> Theory.add_name (get_name thy);
fun checkpoint thy =
if is_draft thy then
@@ -473,7 +478,6 @@
("itself", [logicS], logicS)]
|> Theory.add_nonterminals Syntax.pure_nonterms
|> Theory.add_syntax Syntax.pure_syntax
- |> Theory.add_modesyntax (Symbol.symbolsN, true) Syntax.pure_sym_syntax
|> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
|> Theory.add_trfuns Syntax.pure_trfuns
|> Theory.add_trfunsT Syntax.pure_trfunsT
--- a/src/Pure/sign.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/sign.ML Fri Nov 09 00:19:20 2001 +0100
@@ -148,8 +148,9 @@
val data_kinds: data -> string list
val merge_refs: sg_ref * sg_ref -> sg_ref
val merge: sg * sg -> sg
+ val copy: sg -> sg
+ val finish: sg -> sg
val prep_ext: sg -> sg
- val copy: sg -> sg
val PureN: string
val CPureN: string
val nontriv_merge: sg * sg -> sg
@@ -162,7 +163,8 @@
sig
include SIGN
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
+ (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
val print_data: Object.kind -> sg -> unit
@@ -191,8 +193,9 @@
Data of
(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) * (*copy method*)
+ (Object.T -> Object.T) * (*finish method*)
+ (Object.T -> Object.T) * (*prepare extend method*)
(Object.T * Object.T -> Object.T) * (*merge and prepare extend method*)
(sg -> Object.T -> unit)))) (*print method*)
Symtab.table
@@ -337,9 +340,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 exn => err_method "prep_ext" (Object.name_of_kind kind) exn, mths))
- | merge_entries [(kind, (e1, mths as (_, _, mrg, _))), (_, (e2, _))] =
+ | merge_entries [(kind, (e1, mths as (_, _, _, mrg, _))), (_, (e2, _))] =
(kind, (mrg (e1, e2)
handle exn => err_method "merge" (Object.name_of_kind kind) exn, mths))
| merge_entries _ = sys_error "merge_entries";
@@ -353,9 +356,9 @@
fun prep_ext_data data = merge_data (data, empty_data);
-fun init_data_sg sg (Data tab) kind e cp ext mrg prt =
+fun init_data_sg sg (Data tab) kind e cp fin ext mrg prt =
let val name = Object.name_of_kind kind in
- Data (Symtab.update_new ((name, (kind, (e, (cp, ext, mrg, prt)))), tab))
+ Data (Symtab.update_new ((name, (kind, (e, (cp, fin, ext, mrg, prt)))), tab))
handle Symtab.DUP _ => err_dup_init sg name
end;
@@ -378,7 +381,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 exn => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) exn end;
fun put_data_sg sg (Data tab) kind f x =
@@ -1015,14 +1018,21 @@
(* signature data *)
-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_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, fin, ext, mrg, prt)) =
+ (syn, tsig, ctab, names, init_data_sg sg data kind e cp fin 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, _, _, _))) =
+fun finish_data (k, (e, mths as (_, fin, _, _, _))) =
+ (k, (fin e handle exn => err_method "finish" (Object.name_of_kind k) exn, mths));
+
+fun ext_finish_data (syn, tsig, ctab, names, Data tab) () =
+ (syn, tsig, ctab, names, Data (Symtab.map finish_data tab));
+
+
+fun copy_data (k, (e, mths as (cp, _, _, _, _))) =
(k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths));
fun copy (sg as Sg ({id = _, stamps}, {self, tsig, const_tab, syn, path, spaces, data})) =
@@ -1065,6 +1075,7 @@
val hide_space_i = extend_sign true ext_hide_space_i "#";
fun init_data arg sg = extend_sign true (ext_init_data sg) "#" arg sg;
fun put_data k f x sg = extend_sign true (ext_put_data sg) "#" (k, f, x) sg;
+fun finish sg = extend_sign true ext_finish_data "#" () sg;
fun add_name name sg = extend_sign true K name () sg;
fun prep_ext sg = extend_sign false K "#" () sg;
--- a/src/Pure/theory.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/theory.ML Fri Nov 09 00:19:20 2001 +0100
@@ -86,6 +86,7 @@
val hide_consts: string list -> theory -> theory
val add_name: string -> theory -> theory
val copy: theory -> theory
+ val finish: theory -> theory
val prep_ext: theory -> theory
val prep_ext_merge: theory list -> theory
val requires: theory -> string -> string -> unit
@@ -97,7 +98,8 @@
sig
include THEORY
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
+ (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
val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
@@ -227,6 +229,7 @@
val hide_consts = curry hide_space_i Sign.constK;
val add_name = ext_sign Sign.add_name;
val copy = ext_sign (K Sign.copy) ();
+val finish = ext_sign (K Sign.finish) ();
val prep_ext = ext_sign (K Sign.prep_ext) ();
--- a/src/Pure/theory_data.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/theory_data.ML Fri Nov 09 00:19:20 2001 +0100
@@ -11,6 +11,7 @@
type T
val empty: T
val copy: T -> T
+ val finish: T -> T
val prep_ext: T -> T
val merge: T * T -> T
val print: Sign.sg -> T -> unit
@@ -40,6 +41,7 @@
Theory.init_data kind
(Data Args.empty,
fn (Data x) => Data (Args.copy x),
+ fn (Data x) => Data (Args.finish 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);
--- a/src/Sequents/prover.ML Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Sequents/prover.ML Fri Nov 09 00:19:20 2001 +0100
@@ -174,6 +174,7 @@
type T = pack ref;
val empty = ref empty_pack
fun copy (ref pack) = ref pack;
+ val finish = I;
val prep_ext = copy;
fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
fun print _ (ref pack) = print_pack pack;