# HG changeset patch
# User haftmann
# Date 1648976857 0
# Node ID 010a77180dff799ea4b87b0f60b74e07eb265e97
# Parent  970b9ab6c439f5b0de8d83485ec7e900ed757949
adjusted printing of type annotations to accomodate Scala 3

diff -r 970b9ab6c439 -r 010a77180dff CONTRIBUTORS
--- 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
diff -r 970b9ab6c439 -r 010a77180dff NEWS
--- 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 ***
 
diff -r 970b9ab6c439 -r 010a77180dff src/Tools/Code/code_scala.ML
--- 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) =