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

Hi Christioph,

The new way of writing this is with "code_printing code_module", e.g.:

code_printing code_module "" => (Scala) {*package Foo*}


On 03/10/13 23:49, Christoph LANGE wrote:
Dear code generation wizards,

to make generated Scala code more maintainable I would like to have it
in a named package.  (I'm actually making the code even more
maintainable, albeit somewhat fragile, by splitting it into
objects/classes using,
and this script relies on the package name.)

So far I have been using the following setup for this:

code_include Scala ""
{*package Foo
export_code def1 ... defN in Scala
file "code/Foo.scala"

Isabelle 2013-1-RC1 now warns me:

Legacy feature! prefer "code_printing" for custom serialisations

However code_printing works in the context of symbols IIUC; it can't
just output something at the beginning of the output file.

Should I ignore this warning, or is there a more modern way to achieve
what I want?

Cheers, and thanks in advance,


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