src/Tools/Code/code_scala.ML
changeset 39102 4ae1d212100f
parent 39059 3a11a667af75
child 39142 f63715f00fdd
child 39147 3c284a152bd6
equal deleted inserted replaced
39071:928c5a5bdc93 39102:4ae1d212100f
   387     (* serialization *)
   387     (* serialization *)
   388     val p = Pretty.chunks2 (map snd includes @ the_list (print_nodes [] sca_program));
   388     val p = Pretty.chunks2 (map snd includes @ the_list (print_nodes [] sca_program));
   389     fun write width NONE = writeln o format [] width
   389     fun write width NONE = writeln o format [] width
   390       | write width (SOME p) = File.write p o format [] width;
   390       | write width (SOME p) = File.write p o format [] width;
   391   in
   391   in
   392     Code_Target.serialization write (rpair [] ooo format) p
   392     Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
   393   end;
   393   end;
   394 
   394 
   395 val serializer : Code_Target.serializer =
   395 val serializer : Code_Target.serializer =
   396   Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
   396   Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
   397 
   397