1165 [] => stamps |
1165 [] => stamps |
1166 | dups => error ("Attempt to merge different versions of theories " ^ commas_quote dups)) |
1166 | dups => error ("Attempt to merge different versions of theories " ^ commas_quote dups)) |
1167 end; |
1167 end; |
1168 |
1168 |
1169 |
1169 |
1170 (* trivial merge *) |
1170 (*** trivial merge ***) |
|
1171 |
|
1172 (*For concise error messages: the last few components only*) |
|
1173 fun abbrev_stamp_names_of sg = rev (List.take(map ! (stamps_of sg), 5)); |
|
1174 |
|
1175 fun abbrev_str_of sg = |
|
1176 let val sts = "..., " ^ commas (abbrev_stamp_names_of sg) |
|
1177 handle Subscript => commas (stamp_names_of sg) |
|
1178 in "{" ^ sts ^ "}" end; |
1171 |
1179 |
1172 fun merge_refs (sgr1 as SgRef (SOME (ref (sg1 as Sg ({stamps = s1, ...}, _)))), |
1180 fun merge_refs (sgr1 as SgRef (SOME (ref (sg1 as Sg ({stamps = s1, ...}, _)))), |
1173 sgr2 as SgRef (SOME (ref (sg2 as Sg ({stamps = s2, ...}, _))))) = |
1181 sgr2 as SgRef (SOME (ref (sg2 as Sg ({stamps = s2, ...}, _))))) = |
1174 if subsig (sg2, sg1) then sgr1 |
1182 if subsig (sg2, sg1) then sgr1 |
1175 else if subsig (sg1, sg2) then sgr2 |
1183 else if subsig (sg1, sg2) then sgr2 |
1176 else (merge_stamps s1 s2; (*check for different versions*) |
1184 else (merge_stamps s1 s2; (*check for different versions*) |
1177 error "Attempt to do non-trivial merge of signatures") |
1185 error ("Attempt to do non-trivial merge of signatures\n" ^ |
|
1186 abbrev_str_of sg1 ^ "\n" ^ |
|
1187 abbrev_str_of sg2 ^ "\n")) |
1178 | merge_refs _ = sys_error "Sign.merge_refs"; |
1188 | merge_refs _ = sys_error "Sign.merge_refs"; |
1179 |
1189 |
1180 val merge = deref o merge_refs o pairself self_ref; |
1190 val merge = deref o merge_refs o pairself self_ref; |
1181 |
1191 |
1182 |
1192 |