corrected semantics of presentation_stmt_names; do not print includes on presentation selection
authorhaftmann
Thu, 26 Aug 2010 10:23:25 +0200
changeset 39005eb7bc47f062b
parent 39004 f9cd27cbe8a4
child 39006 f9837065b5e8
corrected semantics of presentation_stmt_names; do not print includes on presentation selection
src/Tools/Code/code_scala.ML
     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)