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



Hello Florian,

>> 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 …).

Could you provide a complete example for me please? And, is it
possible to add some sort of Isabelle version string (such as
"Isabelle2013-1-RC3") to the header?

Thank you very much
  Cornelius




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