309 |
309 |
310 fun project_program thy abortable names_hidden names1 program2 = |
310 fun project_program thy abortable names_hidden names1 program2 = |
311 let |
311 let |
312 val ctxt = Proof_Context.init_global thy; |
312 val ctxt = Proof_Context.init_global thy; |
313 val names2 = subtract (op =) names_hidden names1; |
313 val names2 = subtract (op =) names_hidden names1; |
314 val program3 = Graph.subgraph (not o member (op =) names_hidden) program2; |
314 val program3 = Graph.restrict (not o member (op =) names_hidden) program2; |
315 val names4 = Graph.all_succs program3 names2; |
315 val names4 = Graph.all_succs program3 names2; |
316 val empty_funs = filter_out (member (op =) abortable) |
316 val empty_funs = filter_out (member (op =) abortable) |
317 (Code_Thingol.empty_funs program3); |
317 (Code_Thingol.empty_funs program3); |
318 val _ = |
318 val _ = |
319 if null empty_funs then () |
319 if null empty_funs then () |
320 else error ("No code equations for " ^ |
320 else error ("No code equations for " ^ |
321 commas (map (Proof_Context.extern_const ctxt) empty_funs)); |
321 commas (map (Proof_Context.extern_const ctxt) empty_funs)); |
322 val program4 = Graph.subgraph (member (op =) names4) program3; |
322 val program4 = Graph.restrict (member (op =) names4) program3; |
323 in (names4, program4) end; |
323 in (names4, program4) end; |
324 |
324 |
325 fun prepare_serializer thy abortable serializer literals reserved all_includes |
325 fun prepare_serializer thy abortable serializer literals reserved all_includes |
326 module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax |
326 module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax |
327 module_name args naming proto_program names = |
327 module_name args naming proto_program names = |