src/Tools/Code/code_ml.ML
changeset 38926 24f82786cc57
parent 38924 fcd1d0457e27
child 38928 0e6f54c9d201
equal deleted inserted replaced
38925:ced825abdc1d 38926:24f82786cc57
   900         Long_Name.implode (remainder @ [stmt_name])
   900         Long_Name.implode (remainder @ [stmt_name])
   901       end handle Graph.UNDEF _ =>
   901       end handle Graph.UNDEF _ =>
   902         error ("Unknown statement name: " ^ labelled_name name);
   902         error ("Unknown statement name: " ^ labelled_name name);
   903   in (deresolver, nodes) end;
   903   in (deresolver, nodes) end;
   904 
   904 
   905 fun serialize_ml target print_module print_stmt with_signatures labelled_name
   905 fun serialize_ml target print_module print_stmt with_signatures { labelled_name,
   906   reserved includes single_module module_alias _ tyco_syntax const_syntax program
   906   reserved_syms, includes, single_module, module_alias, class_syntax, tyco_syntax,
   907   (stmt_names, presentation_stmt_names) =
   907   const_syntax, program, names, presentation_names } =
   908   let
   908   let
   909     val is_cons = Code_Thingol.is_cons program;
   909     val is_cons = Code_Thingol.is_cons program;
   910     val is_presentation = not (null presentation_stmt_names);
   910     val is_presentation = not (null presentation_names);
   911     val (deresolver, nodes) = ml_node_of_program labelled_name
   911     val (deresolver, nodes) = ml_node_of_program labelled_name
   912       reserved module_alias program;
   912       reserved_syms module_alias program;
   913     val reserved = make_vars reserved;
   913     val reserved = make_vars reserved_syms;
   914     fun print_node prefix (Dummy _) =
   914     fun print_node prefix (Dummy _) =
   915           NONE
   915           NONE
   916       | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
   916       | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
   917           (null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt
   917           (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
   918           then NONE
   918           then NONE
   919           else SOME (print_stmt labelled_name tyco_syntax const_syntax reserved is_cons (deresolver prefix) stmt)
   919           else SOME (print_stmt labelled_name tyco_syntax const_syntax reserved is_cons (deresolver prefix) stmt)
   920       | print_node prefix (Module (module_name, (_, nodes))) =
   920       | print_node prefix (Module (module_name, (_, nodes))) =
   921           let
   921           let
   922             val (decls, body) = print_nodes (prefix @ [module_name]) nodes;
   922             val (decls, body) = print_nodes (prefix @ [module_name]) nodes;
   925           in SOME ([], p) end
   925           in SOME ([], p) end
   926     and print_nodes prefix nodes = (map_filter (print_node prefix o Graph.get_node nodes)
   926     and print_nodes prefix nodes = (map_filter (print_node prefix o Graph.get_node nodes)
   927         o rev o flat o Graph.strong_conn) nodes
   927         o rev o flat o Graph.strong_conn) nodes
   928       |> split_list
   928       |> split_list
   929       |> (fn (decls, body) => (flat decls, body))
   929       |> (fn (decls, body) => (flat decls, body))
   930     val stmt_names' = map (try (deresolver [])) stmt_names
   930     val names' = map (try (deresolver [])) names
   931       |> single_module ? (map o Option.map) Long_Name.base_name;
   931       |> single_module ? (map o Option.map) Long_Name.base_name;
   932     val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
   932     val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
   933     fun write width NONE = writeln_pretty width
   933     fun write width NONE = writeln_pretty width
   934       | write width (SOME p) = File.write p o string_of_pretty width;
   934       | write width (SOME p) = File.write p o string_of_pretty width;
   935   in
   935   in
   936     Code_Target.serialization write (fn width => (rpair stmt_names' o string_of_pretty width)) p
   936     Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p
   937   end;
   937   end;
   938 
   938 
   939 end; (*local*)
   939 end; (*local*)
   940 
   940 
   941 
   941