--- a/src/Tools/Code/code_ml.ML Thu Sep 02 13:43:38 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Sep 02 13:58:16 2010 +0200
@@ -793,14 +793,15 @@
val is_presentation = not (null presentation_names);
val { deresolver, hierarchical_program = ml_program } =
ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
+ val print_stmt = print_stmt labelled_name tyco_syntax const_syntax
+ (make_vars reserved_syms) is_cons;
fun print_node _ (_, Code_Namespace.Dummy) =
NONE
- | print_node prefix_fragments (_, Code_Namespace.Stmt stmt) =
+ | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
if is_presentation andalso
(null o filter (member (op =) presentation_names) o stmt_names_of) stmt
then NONE
- else SOME (print_stmt labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
- is_cons (deresolver prefix_fragments) stmt)
+ else SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt))
| print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) =
let
val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes;
@@ -815,8 +816,8 @@
|> (fn (decls, body) => (flat decls, body))
val names' = map (try (deresolver [])) names;
val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
- fun write width NONE = writeln o format false width
- | write width (SOME p) = File.write p o format false width;
+ fun write width NONE = writeln o format [] width
+ | write width (SOME p) = File.write p o format [] width;
in
Code_Target.serialization write (rpair names' ooo format) p
end;