src/Tools/Code/code_target.ML
changeset 38936 5cdba14d20fa
parent 38933 bd77e092f67c
child 39034 ebeb48fd653b
equal deleted inserted replaced
38935:2cf3d8305b47 38936:5cdba14d20fa
   296 
   296 
   297 fun project_program thy abortable names_hidden names1 program2 =
   297 fun project_program thy abortable names_hidden names1 program2 =
   298   let
   298   let
   299     val names2 = subtract (op =) names_hidden names1;
   299     val names2 = subtract (op =) names_hidden names1;
   300     val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
   300     val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
   301     val names_all = Graph.all_succs program3 names2;
   301     val names4 = Graph.all_succs program3 names2;
   302     val empty_funs = filter_out (member (op =) abortable)
   302     val empty_funs = filter_out (member (op =) abortable)
   303       (Code_Thingol.empty_funs program3);
   303       (Code_Thingol.empty_funs program3);
   304     val _ = if null empty_funs then () else error ("No code equations for "
   304     val _ = if null empty_funs then () else error ("No code equations for "
   305       ^ commas (map (Sign.extern_const thy) empty_funs));
   305       ^ commas (map (Sign.extern_const thy) empty_funs));
   306   in (names_all, program3) end;
   306     val program4 = Graph.subgraph (member (op =) names4) program3;
       
   307   in (names4, program4) end;
   307 
   308 
   308 fun invoke_serializer thy abortable serializer literals reserved abs_includes 
   309 fun invoke_serializer thy abortable serializer literals reserved abs_includes 
   309     module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
   310     module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
   310     module_name args naming proto_program (names, presentation_names) =
   311     module_name args naming proto_program (names, presentation_names) =
   311   let
   312   let