# HG changeset patch
# User wenzelm
# Date 1712344862 -7200
# Node ID 5afbf04418ec4b481cd533e5c2a17808a930e1e1
# Parent  bda75c790bfa82dd16af3631d6f0859fe247e649
avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax;

diff -r bda75c790bfa -r 5afbf04418ec Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Fri Apr 05 20:41:54 2024 +0200
+++ b/Admin/Release/CHECKLIST	Fri Apr 05 21:21:02 2024 +0200
@@ -24,6 +24,9 @@
 
 - test "isabelle java_monitor -P pid" with "isabelle jedit";
 
+- test "isabelle build HOL-Codegenerator_Test" with -new-syntax
+  (see also etc/settings:ISABELLE_SCALAC_OPTIONS);
+
 - test Windows 10 subsystem for Linux:
   https://docs.microsoft.com/en-us/windows/wsl/install-win10
 
diff -r bda75c790bfa -r 5afbf04418ec NEWS
--- a/NEWS	Fri Apr 05 20:41:54 2024 +0200
+++ b/NEWS	Fri Apr 05 21:21:02 2024 +0200
@@ -38,6 +38,11 @@
 
 *** HOL ***
 
+* Generated Scala code now works both with scalac -new-syntax or
+-old-syntax, but option -no-indent should always be used for robustness.
+Note that ISABELLE_SCALAC_OPTIONS provides options for Isabelle/Scala,
+which are also used for "export_code ... checking Scala".
+
 * Commands 'inductive_cases', 'inductive_simps', 'case_of_simps',
 'simps_of_case' now print results like 'theorem'.
 
diff -r bda75c790bfa -r 5afbf04418ec src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Apr 05 20:41:54 2024 +0200
+++ b/src/HOL/Code_Numeral.thy	Fri Apr 05 21:21:02 2024 +0200
@@ -834,7 +834,7 @@
     (SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)"
     and (OCaml) "!(fun k l ->/ if Z.equal Z.zero l then/ (Z.zero, l) else/ Z.div'_rem/ (Z.abs k)/ (Z.abs l))"
     and (Haskell) "divMod/ (abs _)/ (abs _)"
-    and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))"
+    and (Scala) "!((k: BigInt) => (l: BigInt) =>/ l == 0 match { case true => (BigInt(0), k) case false => (k.abs '/% l.abs) })"
     and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)"
 | constant "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
     (SML) "!((_ : IntInf.int) = _)"
diff -r bda75c790bfa -r 5afbf04418ec src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Apr 05 20:41:54 2024 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 05 21:21:02 2024 +0200
@@ -2067,12 +2067,12 @@
     (SML) "!(if (_)/ then (_)/ else true)"
     and (OCaml) "!(if (_)/ then (_)/ else true)"
     and (Haskell) "!(if (_)/ then (_)/ else True)"
-    and (Scala) "!(if ((_))/ (_)/ else true)"
+    and (Scala) "!((_) match {/ case true => (_)/ case false => true/ })"
 | constant If \<rightharpoonup>
     (SML) "!(if (_)/ then (_)/ else (_))"
     and (OCaml) "!(if (_)/ then (_)/ else (_))"
     and (Haskell) "!(if (_)/ then (_)/ else (_))"
-    and (Scala) "!(if ((_))/ (_)/ else (_))"
+    and (Scala) "!((_) match {/ case true => (_)/ case false => (_)/ })"
 
 code_reserved SML
   not
diff -r bda75c790bfa -r 5afbf04418ec src/HOL/Library/Code_Lazy.thy
--- a/src/HOL/Library/Code_Lazy.thy	Fri Apr 05 20:41:54 2024 +0200
+++ b/src/HOL/Library/Code_Lazy.thy	Fri Apr 05 21:21:02 2024 +0200
@@ -209,10 +209,10 @@
     ty: Typerep,
     x: Lazy[A],
     dummy: Term) : Term = {
-    if (x.evaluated)
-      app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get())))
-    else
-      app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty)))
+    x.evaluated match {
+      case true => app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get())))
+      case false => app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty)))
+    }
   }
 }\<close> for type_constructor lazy constant delay force termify_lazy
 | type_constructor lazy \<rightharpoonup> (Scala) "Lazy.Lazy[_]"
diff -r bda75c790bfa -r 5afbf04418ec src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Apr 05 20:41:54 2024 +0200
+++ b/src/HOL/String.thy	Fri Apr 05 21:21:02 2024 +0200
@@ -803,12 +803,12 @@
     (SML) "Str'_Literal.literal'_of'_asciis"
     and (OCaml) "Str'_Literal.literal'_of'_asciis"
     and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
-    and (Scala) "_.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\")).mkString"
+    and (Scala) "_.map((k: BigInt) => BigInt(0) <= k && k < BigInt(128) match { case true => k.charValue case false => sys.error(\"Non-ASCII character in literal\") }).mkString"
 | constant String.asciis_of_literal \<rightharpoonup>
     (SML) "Str'_Literal.asciis'_of'_literal"
     and (OCaml) "Str'_Literal.asciis'_of'_literal"
     and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"
-    and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))"
+    and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; k < 128 match { case true => BigInt(k) case false => sys.error(\"Non-ASCII character in literal\") } }))"
 | class_instance String.literal :: equal \<rightharpoonup>
     (Haskell) -
 | constant "HOL.equal :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>