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



Hi Cornelius,

> 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 *}

instead of Code_Target.add_include, use Code_Target.set_printings
(Code_Symbol.Module …).

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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