# HG changeset patch
# User wenzelm
# Date 1602356689 -7200
# Node ID 10c07d224035d5598e4652073a0b1f99b9620571
# Parent  f8aa2efce869c626023aa9741ae65fefd2650830
tuned signature;

diff -r f8aa2efce869 -r 10c07d224035 src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala	Sat Oct 10 20:57:08 2020 +0200
+++ b/src/Pure/Admin/build_csdp.scala	Sat Oct 10 21:04:49 2020 +0200
@@ -54,9 +54,9 @@
     verbose: Boolean = false,
     progress: Progress = new Progress,
     target_dir: Path = Path.current,
-    mingw_context: MinGW.Context = MinGW.none)
+    mingw: MinGW = MinGW.none)
   {
-    mingw_context.check
+    mingw.check
 
     Isabelle_System.with_tmp_dir("build")(tmp_dir =>
     {
@@ -123,8 +123,7 @@
             foreach(file => flags.change(File.path(file)))
       }
 
-      progress.bash(mingw_context.bash_command("make"),
-        cwd = build_dir.file, echo = verbose).check
+      progress.bash(mingw.bash_command("make"), cwd = build_dir.file, echo = verbose).check
 
 
       /* install */
@@ -140,7 +139,7 @@
           List("libblas", "liblapack", "libgfortran-5", "libgcc_s_seh-1",
             "libquadmath-0", "libwinpthread-1")
         for (name <- libs) {
-          File.copy(mingw_context.get_root + Path.explode("mingw64/bin") + Path.basic(name).ext("dll"),
+          File.copy(mingw.get_root + Path.explode("mingw64/bin") + Path.basic(name).ext("dll"),
             platform_dir)
         }
       }
@@ -185,7 +184,7 @@
     args =>
     {
       var target_dir = Path.current
-      var mingw_context = MinGW.none
+      var mingw = MinGW.none
       var download_url = default_download_url
       var verbose = false
 
@@ -202,7 +201,7 @@
   Build prover component from official downloads.
 """,
         "D:" -> (arg => target_dir = Path.explode(arg)),
-        "M:" -> (arg => mingw_context = MinGW.context(Path.explode(arg))),
+        "M:" -> (arg => mingw = MinGW.root(Path.explode(arg))),
         "U:" -> (arg => download_url = arg),
         "v" -> (_ => verbose = true))
 
@@ -212,6 +211,6 @@
       val progress = new Console_Progress()
 
       build_csdp(download_url = download_url, verbose = verbose, progress = progress,
-        target_dir = target_dir, mingw_context = mingw_context)
+        target_dir = target_dir, mingw = mingw)
     })
 }
diff -r f8aa2efce869 -r 10c07d224035 src/Pure/System/mingw.scala
--- a/src/Pure/System/mingw.scala	Sat Oct 10 20:57:08 2020 +0200
+++ b/src/Pure/System/mingw.scala	Sat Oct 10 21:04:49 2020 +0200
@@ -9,9 +9,6 @@
 
 object MinGW
 {
-  val none: Context = new Context(None)
-  def context(root: Path) = new Context(Some(root))
-
   def environment: List[(String, String)] =
     List("PATH" -> "/usr/bin:/bin:/mingw64/bin", "CONFIG_SITE" -> "/mingw64/etc/config.site")
 
@@ -19,34 +16,37 @@
     (for ((a, b) <- environment) yield Bash.string(a) + "=" + Bash.string(b))
       .mkString("/usr/bin/env ", " ", " ")
 
-  class Context private[MinGW](val root: Option[Path])
-  {
-    override def toString: String =
-      root match {
-        case None => "MinGW.none"
-        case Some(msys_root) => "MinGW.context(" + msys_root.toString + ")"
-      }
+  val none: MinGW = new MinGW(None)
+  def root(path: Path) = new MinGW(Some(path))
+}
+
+class MinGW private(val root: Option[Path])
+{
+  override def toString: String =
+    root match {
+      case None => "MinGW.none"
+      case Some(msys_root) => "MinGW.root(" + msys_root.toString + ")"
+    }
 
-    def bash_command(command: String): String =
-      root match {
-        case None => command
-        case Some(msys_root) =>
-          File.bash_path(msys_root + Path.explode("usr/bin/bash")) +
-            " -c " + Bash.string(environment_prefix + command)
-      }
+  def bash_command(command: String): String =
+    root match {
+      case None => command
+      case Some(msys_root) =>
+        File.bash_path(msys_root + Path.explode("usr/bin/bash")) +
+          " -c " + Bash.string(MinGW.environment_prefix + command)
+    }
 
-    def get_root: Path =
-      if (!Platform.is_windows) error("Windows platform required")
-      else if (root.isEmpty) error("Windows platform needs specification of msys root directory")
-      else root.get
+  def get_root: Path =
+    if (!Platform.is_windows) error("Windows platform required")
+    else if (root.isEmpty) error("Windows platform needs specification of msys root directory")
+    else root.get
 
-    def check
-    {
-      if (Platform.is_windows) {
-        get_root
-        val result = Isabelle_System.bash(bash_command("uname -s")).check
-        if (!result.out.startsWith("MSYS")) error("Bad msys installation " + get_root)
-      }
+  def check
+  {
+    if (Platform.is_windows) {
+      get_root
+      val result = Isabelle_System.bash(bash_command("uname -s")).check
+      if (!result.out.startsWith("MSYS")) error("Bad msys installation " + get_root)
     }
   }
 }