diff -r 003475955593 -r ef02c5e051e5 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Mon Jan 07 18:50:41 2019 +0100 +++ b/src/Tools/Code/code_scala.ML Thu Jan 10 12:07:05 2019 +0000 @@ -402,7 +402,7 @@ end; fun serialize_scala case_insensitive ctxt { module_name, reserved_syms, identifiers, - includes, class_syntax, tyco_syntax, const_syntax } exports program = + includes, class_syntax, tyco_syntax, const_syntax } program exports = let (* build program *) @@ -438,11 +438,8 @@ @ Code_Namespace.print_hierarchical { print_module = print_module, print_stmt = print_stmt, lift_markup = I } scala_program); - fun write width NONE = writeln o format [] width - | write width (SOME p) = File.write p o format [] width; - fun prepare syms width p = ([("", format syms width p)], try (deresolver [])); in - Code_Target.serialization write prepare p + (Code_Target.Singleton ("scala", p), try (deresolver [])) end; val serializer : Code_Target.serializer =