Email Gateway (Aug 19 2022 at 12:04): Email Gateway (Aug 19 2022 at 12:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Cornelius,
instead of Code_Target.add_include, use Code_Target.set_printings
(Code_Symbol.Module …).
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 12:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
It's correct, although the introducing »No« confuses me.
Florian
signature.asc
Email Gateway (Aug 19 2022 at 12:08):From: "C. Diekmann" <diekmann@in.tum.de>
Hello Florian,
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
Email Gateway (Aug 19 2022 at 12:08):From: Christoph LANGE <math.semantic.web@gmail.com>
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
Email Gateway (Aug 19 2022 at 12:11):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Cornelius,
ML {*
fun scala_header thy =
let
val date = Date.toString (Date.fromTimeLocal (Time.now ()));
val package = "package Foo";
val export_file = Context.theory_name thy ^ ".thy";
val header = package ^ "\n" ^ "// Generated by Isabelle (" ^
Distribution.version ^ ") on " ^ date ^ "\n" ^ "// src: " ^ export_file
^ "\n";
in
Code_Target.set_printings (Code_Symbol.Module ("", [("Scala", SOME
(header, []))])) thy
end
*}
setup {* scala_header *}
export_code distinct in Scala
;-) Florian
signature.asc
Email Gateway (Aug 19 2022 at 12:13):From: "C. Diekmann" <diekmann@in.tum.de>
Hi Florian,
Works like charm. Thank you!
Cornelius
Email Gateway (Aug 19 2022 at 12:14):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Christioph,
The new way of writing this is with "code_printing code_module", e.g.:
code_printing code_module "" => (Scala) {package Foo}
Best,
Andreas
Email Gateway (Aug 19 2022 at 12:18):From: "C. Diekmann" <diekmann@in.tum.de>
Hi Andreas,
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
Email Gateway (Aug 19 2022 at 12:19):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Apr 30 2024 at 16:19 UTC