--- a/CONTRIBUTORS Sun Apr 03 14:48:55 2022 +0100
+++ b/CONTRIBUTORS Sun Apr 03 09:07:37 2022 +0000
@@ -10,7 +10,9 @@
Various improvements to Isabelle/VSCode.
* March 2021: Florian Haftmann, TU München
- More ambitious minimization of case expressions in generated code.
+ More ambitious minimization of case expressions in generated code;
+ code generation: type annotations in pattern bindings are printed in a
+ way suitable for Scala 3.
Contributions to Isabelle2021-1
--- a/NEWS Sun Apr 03 14:48:55 2022 +0100
+++ b/NEWS Sun Apr 03 09:07:37 2022 +0000
@@ -97,6 +97,9 @@
* More ambitious minimization of case expressions in generated code.
+* Code generation for Scala: type annotations in pattern bindings
+ are printed in a way suitable for Scala 3.
+
*** System ***
--- a/src/Tools/Code/code_scala.ML Sun Apr 03 14:48:55 2022 +0100
+++ b/src/Tools/Code/code_scala.ML Sun Apr 03 09:07:37 2022 +0000
@@ -160,8 +160,8 @@
fun print_match_val ((pat, ty), t) vars =
vars
|> print_bind tyvars some_thm BR pat
- |>> (fn p => (false, concat [str "val", constraint p (print_typ tyvars NOBR ty),
- str "=", print_term tyvars false some_thm vars NOBR t]));
+ |>> (fn p => (false, concat [str "val", p, str "=",
+ constraint (print_term tyvars false some_thm vars NOBR t) (print_typ tyvars NOBR ty)]));
fun print_match_seq t vars =
((true, print_term tyvars false some_thm vars NOBR t), vars);
fun print_match is_first ((IVar NONE, ty), t) =