# HG changeset patch
# User wenzelm
# Date 1744210520 -7200
# Node ID 7c9fcf2d6706c70c8137f67f49f272448dc15c8e
# Parent  3125fd1ee69c03fbc277a721576514a98c7d1861
clarified signature: more explicit type Platform_Context;

diff -r 3125fd1ee69c -r 7c9fcf2d6706 src/Pure/Admin/component_polyml.scala
--- a/src/Pure/Admin/component_polyml.scala	Wed Apr 09 15:31:27 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala	Wed Apr 09 16:55:20 2025 +0200
@@ -34,43 +34,41 @@
         setup = MinGW.environment_export,
         libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread")))
 
-  def bash(
-    cwd: Path,
-    platform: Isabelle_Platform,
-    mingw: MinGW,
-    script: String,
-    redirect: Boolean = false,
+  sealed case class Platform_Context(
+    platform: Isabelle_Platform = Isabelle_Platform.self,
+    mingw: MinGW = MinGW.none,
     progress: Progress = new Progress
-  ): Process_Result = {
-    val script1 =
-      if (platform.is_arm && platform.is_macos) {
-        "arch -arch arm64 bash -c " + Bash.string(script)
-      }
-      else mingw.bash_script(script)
-    progress.bash(script1, cwd = cwd, redirect = redirect, echo = progress.verbose)
-  }
+  ) {
+    def standard_path(path: Path): String = mingw.standard_path(path)
+
+    def polyml(arch_64: Boolean): String =
+      (if (arch_64) platform.arch_64 else platform.arch_64_32) + "-" + platform.os_name
+
+    def sha1: String = platform.arch_64 + "-" + platform.os_name
 
-  def polyml_platform(arch_64: Boolean): String = {
-    val platform = Isabelle_Platform.self
-    (if (arch_64) platform.arch_64 else platform.arch_64_32) + "-" + platform.os_name
+    def bash(cwd: Path, script: String, redirect: Boolean = false): Process_Result = {
+      val script1 =
+        if (platform.is_arm && platform.is_macos) {
+          "arch -arch arm64 bash -c " + Bash.string(script)
+        }
+        else mingw.bash_script(script)
+      progress.bash(script1, cwd = cwd, redirect = redirect, echo = progress.verbose)
+    }
   }
 
   def make_polyml(
+    platform_context: Platform_Context,
     root: Path,
     gmp_root: Option[Path] = None,
     sha1_root: Option[Path] = None,
     target_dir: Path = Path.current,
     arch_64: Boolean = false,
-    options: List[String] = Nil,
-    mingw: MinGW = MinGW.none,
-    progress: Progress = new Progress,
+    options: List[String] = Nil
   ): Unit = {
     if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
       error("Bad Poly/ML root directory: " + root)
 
-    val platform = Isabelle_Platform.self
-
-    val sha1_platform = platform.arch_64 + "-" + platform.os_name
+    val platform = platform_context.platform
 
     val info =
       platform_info.getOrElse(platform.os_name,
@@ -88,7 +86,7 @@
         for (opt <- info.options) yield {
           if (opt.startsWith("CFLAGS=") && gmp_root.nonEmpty) {
             val root0 = gmp_root.get.absolute
-            val root1 = mingw.standard_path(root0)
+            val root1 = platform_context.standard_path(root0)
             require(root0.implode == File.bash_path(root0), "Bad directory name " + root0)
             opt + " " + "-I" + root1 + "/include -L" + root1 + "/lib"
           }
@@ -101,7 +99,7 @@
         options1 ::: options2 ::: options ::: options3
     }
 
-    bash(root, platform, mingw,
+    platform_context.bash(root,
       info.setup + "\n" +
       """
         [ -f Makefile ] && make distclean
@@ -110,7 +108,7 @@
           rm -rf target
           make && make install
         } || { echo "Build failed" >&2; exit 2; }
-      """, redirect = true, progress = progress).check
+      """, redirect = true).check
 
 
     /* sha1 library */
@@ -118,10 +116,9 @@
     val sha1_files =
       if (sha1_root.isDefined) {
         val dir1 = sha1_root.get
-        bash(dir1, platform, mingw, "./build " + sha1_platform, redirect = true,
-          progress = progress).check
+        platform_context.bash(dir1, "./build " + platform_context.sha1, redirect = true).check
 
-        val dir2 = dir1 + Path.explode(sha1_platform)
+        val dir2 = dir1 + Path.explode(platform_context.sha1)
         File.read_dir(dir2).map(entry => dir2 + Path.basic(entry))
       }
       else Nil
@@ -129,7 +126,7 @@
 
     /* install */
 
-    val platform_path = Path.explode(polyml_platform(arch_64))
+    val platform_path = Path.explode(platform_context.polyml(arch_64))
 
     val platform_dir = target_dir + platform_path
     Isabelle_System.rm_tree(platform_dir)
@@ -146,7 +143,8 @@
     for (file <- sha1_files) Isabelle_System.copy_file(file, platform_dir)
 
     Executable.libraries_closure(
-      platform_dir + Path.basic("poly").platform_exe, mingw = mingw, filter = info.libs)
+      platform_dir + Path.basic("poly").platform_exe, mingw = platform_context.mingw,
+      filter = info.libs)
 
 
     /* polyc: directory prefix */
@@ -198,8 +196,8 @@
 
 
   def build_polyml(
+    platform_context: Platform_Context,
     options: List[String] = Nil,
-    mingw: MinGW = MinGW.none,
     component_name: String = "",
     gmp_url: String = "",
     polyml_url: String = default_polyml_url,
@@ -207,10 +205,10 @@
     polyml_name: String = default_polyml_name,
     sha1_url: String = default_sha1_url,
     sha1_version: String = default_sha1_version,
-    target_dir: Path = Path.current,
-    progress: Progress = new Progress
+    target_dir: Path = Path.current
   ): Unit = {
-    val platform = Isabelle_Platform.self
+    val platform = platform_context.platform
+    val progress = platform_context.progress
 
 
     /* component */
@@ -244,7 +242,7 @@
             else error("Bad platform " + platform)
 
           progress.echo("Building GMP library ...")
-          bash(gmp_dir, platform, mingw, progress = progress,
+          platform_context.bash(gmp_dir,
             script = Library.make_lines(
               "set -e",
               "./configure --enable-cxx --build=" + platform_arch + "-" + platform_os +
@@ -278,16 +276,15 @@
       init_src_root(component_dir.src, "RootX86.ML", "ROOT.ML")
 
       for (arch_64 <- List(false, true)) {
-        progress.echo("Building " + polyml_platform(arch_64))
+        progress.echo("Building " + platform_context.polyml(arch_64))
         make_polyml(
+          platform_context,
           root = polyml_download,
           gmp_root = gmp_root,
           sha1_root = Some(sha1_download),
           target_dir = component_dir.path,
           arch_64 = arch_64,
-          options = options,
-          mingw = mingw,
-          progress = if (progress.verbose) progress else new Progress)
+          options = options)
       }
     }
 
@@ -404,8 +401,8 @@
             case root :: options => (Path.explode(root), options)
             case Nil => getopts.usage()
           }
-        make_polyml(root, gmp_root = gmp_root, sha1_root = sha1_root,
-          progress = new Console_Progress, arch_64 = arch_64, options = options, mingw = mingw)
+        make_polyml(Platform_Context(mingw = mingw, progress = new Console_Progress),
+          root, gmp_root = gmp_root, sha1_root = sha1_root, arch_64 = arch_64, options = options)
       })
 
   val isabelle_tool2 =
@@ -458,10 +455,11 @@
         val options = getopts(args)
 
         val progress = new Console_Progress(verbose = verbose)
+        val platform_context = Platform_Context(mingw = mingw, progress = progress)
 
-        build_polyml(options = options, mingw = mingw, component_name = component_name,
+        build_polyml(platform_context, options = options, component_name = component_name,
           gmp_url = gmp_url, polyml_url = polyml_url, polyml_version = polyml_version,
           polyml_name = polyml_name, sha1_url = sha1_url, sha1_version = sha1_version,
-          target_dir = target_dir, progress = progress)
+          target_dir = target_dir)
       })
 }