src/Tools/Code/code_ml.ML
changeset 39148 b6530978c14d
parent 39142 f63715f00fdd
parent 39147 3c284a152bd6
child 40627 becf5d5187cc
     1.1 --- a/src/Tools/Code/code_ml.ML	Sat Sep 04 21:12:42 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Sat Sep 04 21:14:40 2010 +0200
     1.3 @@ -785,31 +785,33 @@
     1.4        cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
     1.5    end;
     1.6  
     1.7 -fun serialize_ml target print_module print_stmt with_signatures
     1.8 +fun serialize_ml target print_ml_module print_ml_stmt with_signatures
     1.9      { labelled_name, reserved_syms, includes, module_alias,
    1.10        class_syntax, tyco_syntax, const_syntax, program } =
    1.11    let
    1.12 -    val is_cons = Code_Thingol.is_cons program;
    1.13 +
    1.14 +    (* build program *)
    1.15      val { deresolver, hierarchical_program = ml_program } =
    1.16        ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
    1.17 -    val print_stmt = print_stmt labelled_name tyco_syntax const_syntax
    1.18 -      (make_vars reserved_syms) is_cons;
    1.19 -    fun print_node _ (_, Code_Namespace.Dummy) =
    1.20 -          NONE
    1.21 -      | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
    1.22 -          SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt))
    1.23 -      | print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) =
    1.24 -          let
    1.25 -            val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes;
    1.26 -            val p = print_module name_fragment
    1.27 -                (if with_signatures then SOME decls else NONE) body;
    1.28 -          in SOME ([], p) end
    1.29 -    and print_nodes prefix_fragments nodes = (map_filter
    1.30 -        (fn name => print_node prefix_fragments (name, snd (Graph.get_node nodes name)))
    1.31 -        o rev o flat o Graph.strong_conn) nodes
    1.32 -      |> split_list
    1.33 -      |> (fn (decls, body) => (flat decls, body))
    1.34 -    val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
    1.35 +
    1.36 +    (* print statements *)
    1.37 +    fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
    1.38 +      labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
    1.39 +      (Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt
    1.40 +      |> apfst SOME;
    1.41 +
    1.42 +    (* print modules *)
    1.43 +    fun print_module prefix_fragments base _ xs =
    1.44 +      let
    1.45 +        val (raw_decls, body) = split_list xs;
    1.46 +        val decls = if with_signatures then SOME (maps these raw_decls) else NONE 
    1.47 +      in (NONE, print_ml_module base decls body) end;
    1.48 +
    1.49 +    (* serialization *)
    1.50 +    val p = Pretty.chunks2 (map snd includes
    1.51 +      @ map snd (Code_Namespace.print_hierarchical {
    1.52 +        print_module = print_module, print_stmt = print_stmt,
    1.53 +        lift_markup = apsnd } ml_program));
    1.54      fun write width NONE = writeln o format [] width
    1.55        | write width (SOME p) = File.write p o format [] width;
    1.56    in