# HG changeset patch
# User wenzelm
# Date 1746607509 -7200
# Node ID 2757f73abda7d792a7a9ed80f93dbd92bdde6549
# Parent  cf64152e9f51a667b3a8e82137563ec642dc38de
clarified signature and modules;

diff -r cf64152e9f51 -r 2757f73abda7 src/Pure/Admin/component_polyml.scala
--- a/src/Pure/Admin/component_polyml.scala	Tue May 06 17:03:56 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala	Wed May 07 10:45:09 2025 +0200
@@ -12,67 +12,54 @@
 object Component_PolyML {
   /** platform information **/
 
-  sealed case class Platform_Info(
-    options: List[String] = Nil,
-    setup: String = "",
-    libs: Set[String] = Set.empty)
-
-  sealed case class Platform_Context(
-    platform: Isabelle_Platform = Isabelle_Platform.local,
-    mingw: MinGW = MinGW.none,
-    progress: Progress = new Progress
-  ) {
-    def info: Platform_Info =
+  object Platform_Info {
+    def apply(platform: Isabelle_Platform): Platform_Info =
       if (platform.is_linux) {
         Platform_Info(
+          platform = platform,
           options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"),
           libs = Set("libgmp"))
       }
       else if (platform.is_macos) {
         Platform_Info(
+          platform = platform,
           options = List("CFLAGS=-O3", "CXXFLAGS=-O3", "LDFLAGS=-segprot POLY rwx rwx"),
           setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin",
           libs = Set("libpolyml", "libgmp"))
       }
       else if (platform.is_windows) {
         Platform_Info(
+          platform = platform,
           options =
             List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
           setup = MinGW.env_prefix,
           libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread"))
       }
       else error("Bad platform: " + quote(platform.toString))
+  }
 
-    def standard_path(path: Path): String =
-      mingw.standard_path(File.standard_path(path))
-
+  sealed case class Platform_Info(
+    platform: Isabelle_Platform = Isabelle_Platform.local,
+    options: List[String] = Nil,
+    setup: String = "",
+    libs: Set[String] = Set.empty
+  ) {
     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 execute(cwd: Path, script_lines: String*): Process_Result = {
-      val script = cat_lines("set -e" :: script_lines.toList)
-      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, echo = progress.verbose).check
-    }
   }
 
 
-
   /** build stages **/
 
   def make_polyml_gmp(
-    platform_context: Platform_Context,
+    platform_context: Isabelle_Platform.Context,
     dir: Path,
     options: List[String] = Nil
   ): Path = {
     val progress = platform_context.progress
-    val platform = platform_context.platform
+    val platform = platform_context.isabelle_platform
 
     val platform_arch = if (platform.is_arm) "aarch64" else "x86_64"
     val platform_os =
@@ -105,7 +92,7 @@
   }
 
   def make_polyml(
-    platform_context: Platform_Context,
+    platform_context: Isabelle_Platform.Context,
     root: Path,
     gmp_root: Option[Path] = None,
     sha1_root: Option[Path] = None,
@@ -116,9 +103,8 @@
     if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
       error("Bad Poly/ML root directory: " + root)
 
-    val platform = platform_context.platform
-
-    val info = platform_context.info
+    val platform = platform_context.isabelle_platform
+    val platform_info = Platform_Info(platform)
 
 
     /* configure and make */
@@ -130,8 +116,8 @@
       def detect_CFLAGS(s: String): Boolean = s.startsWith("CFLAGS=")
 
       val info_options =
-        if (info.options.exists(detect_CFLAGS)) info.options
-        else "CFLAGS=" :: info.options
+        if (platform_info.options.exists(detect_CFLAGS)) platform_info.options
+        else "CFLAGS=" :: platform_info.options
 
       val options2 =
         for (opt <- info_options) yield {
@@ -160,7 +146,7 @@
       }
 
     platform_context.execute(root,
-      info.setup,
+      platform_info.setup,
       gmp_setup,
       "[ -f Makefile ] && make distclean",
       """./configure --prefix="$PWD/target" """ + Bash.strings(configure_options),
@@ -174,7 +160,7 @@
     val sha1_files =
       sha1_root match {
         case Some(dir) =>
-          val platform_path = Path.explode(platform_context.sha1)
+          val platform_path = Path.explode(platform_info.sha1)
           val platform_dir = dir + platform_path
           platform_context.execute(dir, "./build " + File.bash_path(platform_path))
           File.read_dir(platform_dir).map(entry => platform_dir + Path.basic(entry))
@@ -184,7 +170,7 @@
 
     /* install */
 
-    val platform_path = Path.explode(platform_context.polyml(arch_64))
+    val platform_path = Path.explode(platform_info.polyml(arch_64))
     val platform_dir = target_dir + platform_path
 
     Isabelle_System.rm_tree(platform_dir)
@@ -200,7 +186,7 @@
       platform_dir + Path.basic("poly").platform_exe,
       env_prefix = gmp_setup + "\n",
       mingw = platform_context.mingw,
-      filter = info.libs)
+      filter = platform_info.libs)
 
 
     /* polyc: directory prefix */
@@ -252,7 +238,7 @@
 
 
   def build_polyml(
-    platform_context: Platform_Context,
+    platform_context: Isabelle_Platform.Context,
     options: List[String] = Nil,
     component_name: String = "",
     gmp_url: String = "",
@@ -264,7 +250,9 @@
     sha1_version: String = default_sha1_version,
     target_dir: Path = Path.current
   ): Unit = {
-    val platform = platform_context.platform
+    val platform = platform_context.isabelle_platform
+    val platform_info = Platform_Info(platform)
+
     val progress = platform_context.progress
 
 
@@ -315,7 +303,7 @@
       init_src_root(component_dir.src, "RootX86.ML", "ROOT.ML")
 
       for (arch_64 <- List(false, true)) {
-        progress.echo("Building Poly/ML " + platform_context.polyml(arch_64))
+        progress.echo("Building Poly/ML " + platform_info.polyml(arch_64))
         make_polyml(
           platform_context,
           root = polyml_download,
@@ -430,9 +418,8 @@
 
         val progress = new Console_Progress(verbose = verbose)
 
-        val target_dir =
-          make_polyml_gmp(Platform_Context(mingw = mingw, progress = progress),
-            root, options = options)
+        val platform_context = Isabelle_Platform.Context(mingw = mingw, progress = progress)
+        val target_dir = make_polyml_gmp(platform_context, root, options = options)
 
         progress.echo("GMP installation directory: " + target_dir)
       })
@@ -478,8 +465,9 @@
           }
 
         val progress = new Console_Progress(verbose = verbose)
-        make_polyml(Platform_Context(mingw = mingw, progress = progress),
-          root, gmp_root = gmp_root, sha1_root = sha1_root, arch_64 = arch_64, options = options)
+        val platform_context = Isabelle_Platform.Context(mingw = mingw, progress = progress)
+        make_polyml(platform_context, root,
+          gmp_root = gmp_root, sha1_root = sha1_root, arch_64 = arch_64, options = options)
       })
 
   val isabelle_tool3 =
@@ -535,7 +523,7 @@
         val options = getopts(args)
 
         val progress = new Console_Progress(verbose = verbose)
-        val platform_context = Platform_Context(mingw = mingw, progress = progress)
+        val platform_context = Isabelle_Platform.Context(mingw = mingw, progress = progress)
 
         build_polyml(platform_context, options = options, component_name = component_name,
           gmp_url = gmp_url, gmp_root = gmp_root, polyml_url = polyml_url,
diff -r cf64152e9f51 -r 2757f73abda7 src/Pure/System/isabelle_platform.scala
--- a/src/Pure/System/isabelle_platform.scala	Tue May 06 17:03:56 2025 +0200
+++ b/src/Pure/System/isabelle_platform.scala	Wed May 07 10:45:09 2025 +0200
@@ -28,6 +28,45 @@
       result.out_lines.map(line =>
         Properties.Eq.unapply(line) getOrElse error("Bad output: " + quote(result.out))))
   }
+
+
+  /* system context for progress/process */
+
+  object Context {
+    def apply(
+      isabelle_platform: Isabelle_Platform = local,
+      mingw: MinGW = MinGW.none,
+      progress: Progress = new Progress
+    ): Context = {
+      val context_platform = isabelle_platform
+      val context_mingw = mingw
+      val context_progress = progress
+      new Context {
+        override def isabelle_platform: Isabelle_Platform = context_platform
+        override def mingw: MinGW = context_mingw
+        override def progress: Progress = context_progress
+      }
+    }
+  }
+
+  trait Context {
+    def isabelle_platform: Isabelle_Platform
+    def mingw: MinGW
+    def progress: Progress
+
+    def standard_path(path: Path): String =
+      mingw.standard_path(File.standard_path(path))
+
+    def execute(cwd: Path, script_lines: String*): Process_Result = {
+      val script = cat_lines("set -e" :: script_lines.toList)
+      val script1 =
+        if (isabelle_platform.is_arm && isabelle_platform.is_macos) {
+          "arch -arch arm64 bash -c " + Bash.string(script)
+        }
+        else mingw.bash_script(script)
+      progress.bash(script1, cwd = cwd, echo = progress.verbose).check
+    }
+  }
 }
 
 class Isabelle_Platform private(val settings: List[(String, String)]) {