# HG changeset patch
# User wenzelm
# Date 1675599239 -3600
# Node ID c42bf52381f1358a463c8d368dc0d0f634ac4b4a
# Parent  f6ba88f2313576f7e170c6933d6f621806bc7b71
proper compiler root for arm64;

diff -r f6ba88f23135 -r c42bf52381f1 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sat Feb 04 23:08:36 2023 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Sun Feb 05 13:13:59 2023 +0100
@@ -160,15 +160,15 @@
   val default_sha1_url = "https://isabelle.sketis.net/repos/sha1/archive"
   val default_sha1_version = "e0239faa6f42"
 
-  private def init_sources(src_dir: Path): Unit = {
-    val lines = split_lines(File.read(src_dir + Path.explode("RootX86.ML")))
+  private def init_src_root(src_dir: Path, input: String, output: String): Unit = {
+    val lines = split_lines(File.read(src_dir + Path.explode(input)))
     val ml_files =
       for {
         line <- lines
         rest <- Library.try_unprefix("use", line)
       } yield "ML_file" + rest
 
-    File.write(src_dir + Path.explode("ROOT.ML"),
+    File.write(src_dir + Path.explode(output),
 """(* Poly/ML Compiler root file.
 
 When this file is open in the Prover IDE, the ML files of the Poly/ML
@@ -215,7 +215,8 @@
           download
         }
 
-      init_sources(component_dir.src)
+      init_src_root(component_dir.src, "RootArm64.ML", "ROOT0.ML")
+      init_src_root(component_dir.src, "RootX86.ML", "ROOT.ML")
 
       for (arch_64 <- List(false, true)) {
         progress.echo("Building " + polyml_platform(arch_64))
@@ -261,7 +262,14 @@
 ML_HOME="$POLYML_HOME/$ML_PLATFORM"
 ML_SOURCES="$POLYML_HOME/src"
 
-ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:\$ML_SOURCES/ROOT.ML"
+case "$ML_PLATFORM" in
+  *arm64*)
+    ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:\$ML_SOURCES/ROOT0.ML"
+    ;;
+  *)
+    ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:\$ML_SOURCES/ROOT.ML"
+    ;;
+esac
 """)