data: removed obsolete finish method;
authorwenzelm
Wed Nov 28 00:44:37 2001 +0100 (2001-11-28)
changeset 1231026407b087c8e
parent 12309 03e9287be350
child 12311 ce5f9e61c037
data: removed obsolete finish method;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Wed Nov 28 00:43:50 2001 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Nov 28 00:44:37 2001 +0100
     1.3 @@ -149,7 +149,6 @@
     1.4    val merge_refs: sg_ref * sg_ref -> sg_ref
     1.5    val merge: sg * sg -> sg
     1.6    val copy: sg -> sg
     1.7 -  val finish: sg -> sg
     1.8    val prep_ext: sg -> sg
     1.9    val PureN: string
    1.10    val CPureN: string
    1.11 @@ -163,8 +162,7 @@
    1.12  sig
    1.13    include SIGN
    1.14    val init_data: Object.kind * (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
    1.15 -    (Object.T -> Object.T) * (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit))
    1.16 -    -> sg -> sg
    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    val print_data: Object.kind -> sg -> unit
    1.21 @@ -194,7 +192,6 @@
    1.22      (Object.kind *                              (*kind (for authorization)*)
    1.23        (Object.T *                               (*value*)
    1.24          ((Object.T -> Object.T) *               (*copy method*)
    1.25 -          (Object.T -> Object.T) *              (*finish method*)
    1.26            (Object.T -> Object.T) *              (*prepare extend method*)
    1.27            (Object.T * Object.T -> Object.T) *   (*merge and prepare extend method*)
    1.28            (sg -> Object.T -> unit))))           (*print method*)
    1.29 @@ -340,9 +337,9 @@
    1.30         None => []
    1.31       | Some x => [(kind, x)]);
    1.32  
    1.33 -    fun merge_entries [(kind, (e, mths as (_, _, ext, _, _)))] =
    1.34 +    fun merge_entries [(kind, (e, mths as (_, ext, _, _)))] =
    1.35            (kind, (ext e handle exn => err_method "prep_ext" (Object.name_of_kind kind) exn, mths))
    1.36 -      | merge_entries [(kind, (e1, mths as (_, _, _, mrg, _))), (_, (e2, _))] =
    1.37 +      | merge_entries [(kind, (e1, mths as (_, _, mrg, _))), (_, (e2, _))] =
    1.38            (kind, (mrg (e1, e2)
    1.39              handle exn => err_method "merge" (Object.name_of_kind kind) exn, mths))
    1.40        | merge_entries _ = sys_error "merge_entries";
    1.41 @@ -356,9 +353,9 @@
    1.42  
    1.43  fun prep_ext_data data = merge_data (data, empty_data);
    1.44  
    1.45 -fun init_data_sg sg (Data tab) kind e cp fin ext mrg prt =
    1.46 +fun init_data_sg sg (Data tab) kind e cp ext mrg prt =
    1.47    let val name = Object.name_of_kind kind in
    1.48 -    Data (Symtab.update_new ((name, (kind, (e, (cp, fin, ext, mrg, prt)))), tab))
    1.49 +    Data (Symtab.update_new ((name, (kind, (e, (cp, ext, mrg, prt)))), tab))
    1.50        handle Symtab.DUP _ => err_dup_init sg name
    1.51    end;
    1.52  
    1.53 @@ -381,7 +378,7 @@
    1.54    in f x handle Match => Object.kind_error kind end;
    1.55  
    1.56  fun print_data kind (sg as Sg (_, {data = Data tab, ...})) =
    1.57 -  let val (e, (_, _, _, _, prt)) = lookup_data sg tab kind
    1.58 +  let val (e, (_, _, _, prt)) = lookup_data sg tab kind
    1.59    in prt sg e handle exn => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) exn end;
    1.60  
    1.61  fun put_data_sg sg (Data tab) kind f x =
    1.62 @@ -1018,21 +1015,14 @@
    1.63  
    1.64  (* signature data *)
    1.65  
    1.66 -fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, fin, ext, mrg, prt)) =
    1.67 -  (syn, tsig, ctab, names, init_data_sg sg data kind e cp fin ext mrg prt);
    1.68 +fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, ext, mrg, prt)) =
    1.69 +  (syn, tsig, ctab, names, init_data_sg sg data kind e cp ext mrg prt);
    1.70  
    1.71  fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, f, x) =
    1.72    (syn, tsig, ctab, names, put_data_sg sg data kind f x);
    1.73  
    1.74  
    1.75 -fun finish_data (k, (e, mths as (_, fin, _, _, _))) =
    1.76 -  (k, (fin e handle exn => err_method "finish" (Object.name_of_kind k) exn, mths));
    1.77 -
    1.78 -fun ext_finish_data (syn, tsig, ctab, names, Data tab) () =
    1.79 -  (syn, tsig, ctab, names, Data (Symtab.map finish_data tab));
    1.80 -
    1.81 -
    1.82 -fun copy_data (k, (e, mths as (cp, _, _, _, _))) =
    1.83 +fun copy_data (k, (e, mths as (cp, _, _, _))) =
    1.84    (k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths));
    1.85  
    1.86  fun copy (sg as Sg ({id = _, stamps}, {self, tsig, const_tab, syn, path, spaces, data})) =
    1.87 @@ -1075,7 +1065,6 @@
    1.88  val hide_space_i      = extend_sign true ext_hide_space_i "#";
    1.89  fun init_data arg sg  = extend_sign true (ext_init_data sg) "#" arg sg;
    1.90  fun put_data k f x sg = extend_sign true (ext_put_data sg) "#" (k, f, x) sg;
    1.91 -fun finish sg         = extend_sign true ext_finish_data "#" () sg;
    1.92  fun add_name name sg  = extend_sign true K name () sg;
    1.93  fun prep_ext sg       = extend_sign false K "#" () sg;
    1.94