src/Tools/Code/code_scala.ML
changeset 38915 026526cba0e6
parent 38913 d1d4d808be26
child 38916 c0b857a04758
     1.1 --- a/src/Tools/Code/code_scala.ML	Mon Aug 30 16:25:04 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Mon Aug 30 16:31:38 2010 +0200
     1.3 @@ -480,10 +480,10 @@
     1.4      val p_includes = if null presentation_stmt_names
     1.5        then map (fn (base, p) => print_module base [] p) includes else [];
     1.6      val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
     1.7 +    fun write width NONE = writeln_pretty width
     1.8 +      | write width (SOME p) = File.write p o string_of_pretty width;
     1.9    in
    1.10 -    Code_Target.mk_serialization
    1.11 -      (fn width => (fn NONE => writeln_pretty width | SOME file => File.write file o string_of_pretty width))
    1.12 -      (rpair [] oo string_of_pretty) p
    1.13 +    Code_Target.mk_serialization write (rpair [] oo string_of_pretty) p
    1.14    end;
    1.15  
    1.16  end; (*local*)