338 fun entry data kind = |
335 fun entry data kind = |
339 (case gen_assoc Object.eq_kind (data, kind) of |
336 (case gen_assoc Object.eq_kind (data, kind) of |
340 None => [] |
337 None => [] |
341 | Some x => [(kind, x)]); |
338 | Some x => [(kind, x)]); |
342 |
339 |
343 fun merge_entries [(kind, (e, mths as (_, _, ext, _, _)))] = |
340 fun merge_entries [(kind, (e, mths as (_, ext, _, _)))] = |
344 (kind, (ext e handle exn => err_method "prep_ext" (Object.name_of_kind kind) exn, mths)) |
341 (kind, (ext e handle exn => err_method "prep_ext" (Object.name_of_kind kind) exn, mths)) |
345 | merge_entries [(kind, (e1, mths as (_, _, _, mrg, _))), (_, (e2, _))] = |
342 | merge_entries [(kind, (e1, mths as (_, _, mrg, _))), (_, (e2, _))] = |
346 (kind, (mrg (e1, e2) |
343 (kind, (mrg (e1, e2) |
347 handle exn => err_method "merge" (Object.name_of_kind kind) exn, mths)) |
344 handle exn => err_method "merge" (Object.name_of_kind kind) exn, mths)) |
348 | merge_entries _ = sys_error "merge_entries"; |
345 | merge_entries _ = sys_error "merge_entries"; |
349 |
346 |
350 val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds; |
347 val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds; |
354 handle Symtab.DUPS dups => err_inconsistent dups |
351 handle Symtab.DUPS dups => err_inconsistent dups |
355 end; |
352 end; |
356 |
353 |
357 fun prep_ext_data data = merge_data (data, empty_data); |
354 fun prep_ext_data data = merge_data (data, empty_data); |
358 |
355 |
359 fun init_data_sg sg (Data tab) kind e cp fin ext mrg prt = |
356 fun init_data_sg sg (Data tab) kind e cp ext mrg prt = |
360 let val name = Object.name_of_kind kind in |
357 let val name = Object.name_of_kind kind in |
361 Data (Symtab.update_new ((name, (kind, (e, (cp, fin, ext, mrg, prt)))), tab)) |
358 Data (Symtab.update_new ((name, (kind, (e, (cp, ext, mrg, prt)))), tab)) |
362 handle Symtab.DUP _ => err_dup_init sg name |
359 handle Symtab.DUP _ => err_dup_init sg name |
363 end; |
360 end; |
364 |
361 |
365 |
362 |
366 (* access data *) |
363 (* access data *) |
379 fun get_data kind f (sg as Sg (_, {data = Data tab, ...})) = |
376 fun get_data kind f (sg as Sg (_, {data = Data tab, ...})) = |
380 let val x = fst (lookup_data sg tab kind) |
377 let val x = fst (lookup_data sg tab kind) |
381 in f x handle Match => Object.kind_error kind end; |
378 in f x handle Match => Object.kind_error kind end; |
382 |
379 |
383 fun print_data kind (sg as Sg (_, {data = Data tab, ...})) = |
380 fun print_data kind (sg as Sg (_, {data = Data tab, ...})) = |
384 let val (e, (_, _, _, _, prt)) = lookup_data sg tab kind |
381 let val (e, (_, _, _, prt)) = lookup_data sg tab kind |
385 in prt sg e handle exn => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) exn end; |
382 in prt sg e handle exn => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) exn end; |
386 |
383 |
387 fun put_data_sg sg (Data tab) kind f x = |
384 fun put_data_sg sg (Data tab) kind f x = |
388 Data (Symtab.update ((Object.name_of_kind kind, |
385 Data (Symtab.update ((Object.name_of_kind kind, |
389 (kind, (f x, snd (lookup_data sg tab kind)))), tab)); |
386 (kind, (f x, snd (lookup_data sg tab kind)))), tab)); |
1016 (syn, tsig, ctab, (path, hide_names spaces kind names), data); |
1013 (syn, tsig, ctab, (path, hide_names spaces kind names), data); |
1017 |
1014 |
1018 |
1015 |
1019 (* signature data *) |
1016 (* signature data *) |
1020 |
1017 |
1021 fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, fin, ext, mrg, prt)) = |
1018 fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, ext, mrg, prt)) = |
1022 (syn, tsig, ctab, names, init_data_sg sg data kind e cp fin ext mrg prt); |
1019 (syn, tsig, ctab, names, init_data_sg sg data kind e cp ext mrg prt); |
1023 |
1020 |
1024 fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, f, x) = |
1021 fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, f, x) = |
1025 (syn, tsig, ctab, names, put_data_sg sg data kind f x); |
1022 (syn, tsig, ctab, names, put_data_sg sg data kind f x); |
1026 |
1023 |
1027 |
1024 |
1028 fun finish_data (k, (e, mths as (_, fin, _, _, _))) = |
1025 fun copy_data (k, (e, mths as (cp, _, _, _))) = |
1029 (k, (fin e handle exn => err_method "finish" (Object.name_of_kind k) exn, mths)); |
|
1030 |
|
1031 fun ext_finish_data (syn, tsig, ctab, names, Data tab) () = |
|
1032 (syn, tsig, ctab, names, Data (Symtab.map finish_data tab)); |
|
1033 |
|
1034 |
|
1035 fun copy_data (k, (e, mths as (cp, _, _, _, _))) = |
|
1036 (k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths)); |
1026 (k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths)); |
1037 |
1027 |
1038 fun copy (sg as Sg ({id = _, stamps}, {self, tsig, const_tab, syn, path, spaces, data})) = |
1028 fun copy (sg as Sg ({id = _, stamps}, {self, tsig, const_tab, syn, path, spaces, data})) = |
1039 let |
1029 let |
1040 val _ = check_stale sg; |
1030 val _ = check_stale sg; |
1073 val add_space = extend_sign true ext_add_space "#"; |
1063 val add_space = extend_sign true ext_add_space "#"; |
1074 val hide_space = extend_sign true ext_hide_space "#"; |
1064 val hide_space = extend_sign true ext_hide_space "#"; |
1075 val hide_space_i = extend_sign true ext_hide_space_i "#"; |
1065 val hide_space_i = extend_sign true ext_hide_space_i "#"; |
1076 fun init_data arg sg = extend_sign true (ext_init_data sg) "#" arg sg; |
1066 fun init_data arg sg = extend_sign true (ext_init_data sg) "#" arg sg; |
1077 fun put_data k f x sg = extend_sign true (ext_put_data sg) "#" (k, f, x) sg; |
1067 fun put_data k f x sg = extend_sign true (ext_put_data sg) "#" (k, f, x) sg; |
1078 fun finish sg = extend_sign true ext_finish_data "#" () sg; |
|
1079 fun add_name name sg = extend_sign true K name () sg; |
1068 fun add_name name sg = extend_sign true K name () sg; |
1080 fun prep_ext sg = extend_sign false K "#" () sg; |
1069 fun prep_ext sg = extend_sign false K "#" () sg; |
1081 |
1070 |
1082 |
1071 |
1083 |
1072 |