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



Hi Cornelius,

No, code_printing code_module can deal only with fixed strings. It is just a new front-end syntax for the same underlying machinery of code_include.

@Florian: Please correct me if I am wrong.

Best,
Andreas

On 07/10/13 16:57, C. Diekmann wrote:
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.