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



Hi Andreas,

2013/10/4 Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>:
> The new way of writing this is with "code_printing code_module", e.g.:
>
> code_printing code_module "" => (Scala) {*package Foo*}

is there a way to translate the following into the new way?
ML {*
val scala_header =
  let
    val package = "package Foo";
    val date = Date.toString (Date.fromTimeLocal (Time.now ()))
    val export_file = Context.theory_name @{theory} ^ ".thy"
    val header = package ^ "\n" ^ "// Generated by Isabelle on " ^
date ^ "\n" ^ "// src: " ^ export_file ^ "\n"
  in
    Code_Target.add_include "Scala" ("", SOME (header, []))
  end
*}
 setup {* scala_header *}

Cheers
  Cornelius




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