corrected semantics of presentation_stmt_names; do not print includes on presentation selection
1.1 --- a/src/Tools/Code/code_scala.ML Thu Aug 26 10:16:22 2010 +0200
1.2 +++ b/src/Tools/Code/code_scala.ML Thu Aug 26 10:23:25 2010 +0200
1.3 @@ -446,8 +446,8 @@
1.4 ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
1.5 @ [p, str ("} /* object " ^ base ^ " */")]);
1.6 fun print_node (_, Dummy) = NONE
1.7 - | print_node (name, Stmt stmt) = if not (not (null presentation_stmt_names)
1.8 - andalso member (op =) presentation_stmt_names name)
1.9 + | print_node (name, Stmt stmt) = if null presentation_stmt_names
1.10 + orelse member (op =) presentation_stmt_names name
1.11 then SOME (print_stmt (name, stmt))
1.12 else NONE
1.13 | print_node (name, Module (_, (implicits, nodes))) = if null presentation_stmt_names
1.14 @@ -462,8 +462,9 @@
1.15 in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
1.16
1.17 (* serialization *)
1.18 - val p = Pretty.chunks2 (map (fn (base, p) => print_module base [] p) includes
1.19 - @ the_list (print_nodes sca_program));
1.20 + val p_includes = if null presentation_stmt_names
1.21 + then map (fn (base, p) => print_module base [] p) includes else [];
1.22 + val p = Pretty.chunks2 (p_includes @ the_list (print_nodes sca_program));
1.23 in
1.24 Code_Target.mk_serialization target
1.25 (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)