Re: [isabelle] 2013-1-RC1: how to put generated Scala into a package without using code_include?



Hi Florian,


2013/10/22 Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
> ML {*
> fun scala_header thy =
>   let
>     val date = Date.toString (Date.fromTimeLocal (Time.now ()));
>     val package = "package Foo";
>     val export_file = Context.theory_name thy ^ ".thy";
>     val header = package ^ "\n" ^ "// Generated by Isabelle (" ^
> Distribution.version ^ ") on " ^ date ^ "\n" ^ "// src: " ^ export_file
> ^ "\n";
>   in
>     Code_Target.set_printings (Code_Symbol.Module ("", [("Scala", SOME
> (header, []))])) thy
>   end
> *}
> setup {* scala_header *}
>
> export_code distinct in Scala

Works like charm. Thank you!

  Cornelius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.