Email Gateway (Aug 23 2022 at 13:17): Email Gateway (Aug 23 2022 at 13:17):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi,
in Isabelle2022-RC0, when exporting Scala code, generated strings will
be encoded in a technically correct but very hard to read way. Consider
the following theory:
theory Scratch
imports Main
begin
generate_file "test.scala" = ‹val test = ‹\<^type_name>‹int›››
export_generated_files _
end
It generates the file test.scala with content:
/* generated by Isabelle */
val test = "\u0049\u006E\u0074\u002E\u0069\u006E\u0074"
While this is valid Scala, I think it would be better to encode at least
printable characters in the ASCII ranges (except " and \ of course)
directly instead of using \u-sequences.
Best wishes,
Dominique.
Email Gateway (Aug 25 2022 at 22:23):From: Makarius <makarius@sketis.net>
OK, I have changed that here for Isabelle2022 release:
https://isabelle-dev.sketis.net/rISABELLEfd9734380709
Side-remark: I've found the subject line confusing, thinking of Scala code
generation from HOL specifications. In contrast, the 'generate_file' facility
is just for adhoc source text, with optional inlining of string values from
Isabelle/ML (including ML antiquotations).
I've added .scala and .java files only recently for Isabelle2022, in order to
support Isabelle/Scala/Java components provided by Isabelle/ML (exported into
the session build database). This already works quite well, although it lacks
PIDE support for Scala.
It also lacks IntelliJ IDEA support, and some weeks ago IntelliJ somehow
stopped working for regular Isabelle/Scala development.
I am glad that Isabelle/PIDE is self-contained and usually works. At some
later stage, the Scala 3 IDE support that I've seen in the sources of the
dotty compiler will probably make it into PIDE. (Not for the Isabelle2022
release.)
Makarius
Email Gateway (Sep 19 2022 at 09:22):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I can confirm that it works fine for me now in Isabelle2022-RC2.
Best wishes,
Dominique.
Last updated: Jan 04 2025 at 20:18 UTC