src/Tools/Code/code_scala.ML
changeset 69623 ef02c5e051e5
parent 68034 27ba50c79328
child 72295 aafec95bc30e
--- 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 =