--- a/src/Pure/sign.ML Wed Nov 28 00:43:50 2001 +0100
+++ b/src/Pure/sign.ML Wed Nov 28 00:44:37 2001 +0100
@@ -149,7 +149,6 @@
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 PureN: string
val CPureN: string
@@ -163,8 +162,7 @@
sig
include SIGN
val init_data: Object.kind * (Object.T * (Object.T -> 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) * (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
@@ -194,7 +192,6 @@
(Object.kind * (*kind (for authorization)*)
(Object.T * (*value*)
((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*)
@@ -340,9 +337,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";
@@ -356,9 +353,9 @@
fun prep_ext_data data = merge_data (data, empty_data);
-fun init_data_sg sg (Data tab) kind e cp fin 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, (cp, fin, 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;
@@ -381,7 +378,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 =
@@ -1018,21 +1015,14 @@
(* signature data *)
-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_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 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, _, _, _, _))) =
+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})) =
@@ -1075,7 +1065,6 @@
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;