# HG changeset patch
# User wenzelm
# Date 1005261560 -3600
# Node ID 739eba13e2cddd9c7d63fa581933b682f04de450
# Parent  7f8d88ed4f21cc5e352a4f1639976eb89ffbe1ce
theory data: finish method;

diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/Isar/attrib.ML
--- 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}) =
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/Isar/calculation.ML
--- 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;
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/Isar/induct_attrib.ML
--- 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))) =
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/Isar/object_logic.ML
--- 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) =
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/Isar/proof_context.ML
--- 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;
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/Thy/present.ML
--- 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 _ _ = ();
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/axclass.ML
--- 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);
 
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/codegen.ML
--- 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},
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/goals.ML
--- 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 = _}) =
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/proofterm.ML
--- 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,
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/pure_thy.ML
--- 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
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/sign.ML
--- 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;
 
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/theory.ML
--- 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) ();
 
 
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Pure/theory_data.ML
--- 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);
diff -r 7f8d88ed4f21 -r 739eba13e2cd src/Sequents/prover.ML
--- 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;