# HG changeset patch
# User wenzelm
# Date 1663418741 -7200
# Node ID d27ed188e0c4b2e7bf841353ed1137ea96c7c3d4
# Parent  322f2e2799a7babefb54b736d875cc34e239b7de
support for ISABELLE_MLTON_OPTIONS, notably for Ubuntu 22.04 with external mlton executable;

diff -r 322f2e2799a7 -r d27ed188e0c4 etc/settings
--- a/etc/settings	Sat Sep 17 12:12:22 2022 +0200
+++ b/etc/settings	Sat Sep 17 14:45:41 2022 +0200
@@ -167,5 +167,6 @@
 ISABELLE_FONTFORGE="fontforge"
 
 #ISABELLE_MLTON="/usr/bin/mlton"
+#ISABELLE_MLTON_OPTIONS="-pi-style npi"
 #ISABELLE_SMLNJ="/usr/bin/sml"
 #ISABELLE_SWIPL="/usr/bin/swipl"
diff -r 322f2e2799a7 -r d27ed188e0c4 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Sat Sep 17 12:12:22 2022 +0200
+++ b/src/HOL/Library/code_test.ML	Sat Sep 17 14:45:41 2022 +0200
@@ -352,8 +352,10 @@
     val _ = File.write driver_path driver
     val _ = File.write basis_path ("$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN)
   in
-    compile compiler ("\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path);
-    evaluate compiler (File.bash_path (dir + Path.basic projectN))
+    compile compiler
+      (\<^verbatim>\<open>"$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf \<close> ^
+        File.bash_platform_path basis_path);
+    evaluate compiler (File.bash_platform_path (dir + Path.basic projectN))
   end
 
 
diff -r 322f2e2799a7 -r d27ed188e0c4 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Sep 17 12:12:22 2022 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Sep 17 14:45:41 2022 +0200
@@ -309,7 +309,7 @@
           options = "-m32 -B -M4" +
             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
             " -e ISABELLE_GHC_SETUP=true" +
-            " -e ISABELLE_MLTON=mlton" +
+            " -e ISABELLE_MLTON=mlton -e ISABELLE_MLTON_OPTIONS=" +
             " -e ISABELLE_SMLNJ=sml" +
             " -e ISABELLE_SWIPL=swipl",
           args = "-a -d '~~/src/Benchmarks'")),
@@ -323,7 +323,7 @@
           options = "-m32 -B -M1x2,2,4 -p pide_session=false" +
             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
             " -e ISABELLE_GHC_SETUP=true" +
-            " -e ISABELLE_MLTON=/usr/local/bin/mlton" +
+            " -e ISABELLE_MLTON=/usr/local/bin/mlton -e ISABELLE_MLTON_OPTIONS=" +
             " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
             " -e ISABELLE_SWIPL=/usr/local/bin/swipl",
           args = "-a -d '~~/src/Benchmarks'")),
@@ -332,7 +332,7 @@
           options = "-m32 -B -M1x2,2,4 -p pide_session=false" +
             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
             " -e ISABELLE_GHC_SETUP=true" +
-            " -e ISABELLE_MLTON=/usr/local/bin/mlton" +
+            " -e ISABELLE_MLTON=/usr/local/bin/mlton -e ISABELLE_MLTON_OPTIONS=" +
             " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
             " -e ISABELLE_SWIPL=/usr/local/bin/swipl",
           args = "-a -d '~~/src/Benchmarks'"),
@@ -375,7 +375,7 @@
           java_heap = "8g",
           options = "-m32 -M1x6 -t AFP" +
             " -e ISABELLE_GHC=ghc" +
-            " -e ISABELLE_MLTON=mlton" +
+            " -e ISABELLE_MLTON=mlton -e ISABELLE_MLTON_OPTIONS=" +
             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
             " -e ISABELLE_SMLNJ=sml",
           args = "-a -X large -X slow",