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



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
https://github.com/formare/auctions/blob/master/isabelle/Auction/code/split-scala-modules.pl,
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,

Christoph

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Mathematics in Computer Science Special Issue on “Enabling Domain
  Experts to use Formalised Reasoning”; submission until 31 October.
  http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/




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