# HG changeset patch
# User wenzelm
# Date 1669841635 -3600
# Node ID 9fe5d8c703521b23e213fa1b0d9a6ad235ea14c5
# Parent  88cecb9f1cdc3e6771eb063857fadd4b11eb5027
tuned signature;

diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_csdp.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -76,7 +76,7 @@
 
       val component_name = "csdp-" + version
       val component_dir =
-        Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+        Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
 
       /* platform */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_cvc5.scala
--- a/src/Pure/Admin/build_cvc5.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_cvc5.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -40,7 +40,7 @@
 
     val component = "cvc5-" + version
     val component_dir =
-      Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+      Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
 
     /* download executables */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_e.scala
--- a/src/Pure/Admin/build_e.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_e.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -25,7 +25,7 @@
 
       val component_name = "e-" + version
       val component_dir =
-        Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+        Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
       val platform_name =
         proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_easychair.scala
--- a/src/Pure/Admin/build_easychair.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_easychair.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -38,7 +38,7 @@
 
         val component = "easychair-" + version
         val component_dir =
-          Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+          Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
         Isabelle_System.extract(download_file, component_dir.path, strip = true)
 
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_eptcs.scala
--- a/src/Pure/Admin/build_eptcs.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_eptcs.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -27,7 +27,7 @@
 
     val component = "eptcs-" + version
     val component_dir =
-      Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+      Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
 
     /* download */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_foiltex.scala
--- a/src/Pure/Admin/build_foiltex.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_foiltex.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -42,7 +42,7 @@
 
         val component = "foiltex-" + version
         val component_dir =
-          Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+          Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
         Isabelle_System.extract(download_file, component_dir.path, strip = true)
 
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_fonts.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -236,7 +236,7 @@
         val component_date = Date.Format.alt_date(Date.now())
         val component_name = "isabelle_fonts-" + component_date
         val component_dir =
-          Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+          Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
         for (hinted <- hinting) {
           Isabelle_System.make_directory(component_dir.path + make_path(hinted = hinted))
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_jdk.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -50,7 +50,7 @@
 
     val component = "jdk-" + jdk_version
     val component_dir =
-      Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+      Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
 
     /* download */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_jedit.scala
--- a/src/Pure/Admin/build_jedit.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_jedit.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -112,7 +112,7 @@
     Isabelle_System.require_command("ant", test = "-version")
     Isabelle_System.require_command("patch")
 
-    val component_dir = Components.Directory.create(component_path, progress = progress)
+    val component_dir = Components.Directory(component_path).create(progress = progress)
 
 
     /* jEdit directory */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_lipics.scala
--- a/src/Pure/Admin/build_lipics.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_lipics.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -53,7 +53,7 @@
 
         val component = "lipics-" + version
         val component_dir =
-          Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+          Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
         Isabelle_System.copy_dir(lipics_dir, component_dir.path)
 
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_llncs.scala
--- a/src/Pure/Admin/build_llncs.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_llncs.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -45,7 +45,7 @@
 
         val component = "llncs-" + version
         val component_dir =
-          Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+          Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
         Isabelle_System.extract(download_file, component_dir.path, strip = true)
 
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_minisat.scala
--- a/src/Pure/Admin/build_minisat.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_minisat.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -42,7 +42,7 @@
 
       val component = proper_string(component_name) getOrElse make_component_name(version)
       val component_dir =
-        Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+        Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
 
       /* platform */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_pdfjs.scala
--- a/src/Pure/Admin/build_pdfjs.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_pdfjs.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -29,7 +29,7 @@
 
     val component = "pdfjs-" + version
     val component_dir =
-      Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+      Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
 
     /* download */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -175,7 +175,7 @@
     component_path: Path,
     sha1_root: Option[Path] = None
   ): Unit = {
-    val component_dir = Components.Directory.create(component_path)
+    val component_dir = Components.Directory(component_path).create()
     extract_sources(source_archive, component_path)
 
     Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/settings"), component_dir.etc)
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_postgresql.scala
--- a/src/Pure/Admin/build_postgresql.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_postgresql.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -37,7 +37,7 @@
     /* component */
 
     val component_dir =
-      Components.Directory.create(target_dir + Path.basic(download_name), progress = progress)
+      Components.Directory(target_dir + Path.basic(download_name)).create(progress = progress)
 
 
     /* LICENSE */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_prismjs.scala
--- a/src/Pure/Admin/build_prismjs.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_prismjs.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -28,7 +28,7 @@
 
     val component = "prismjs-" + version
     val component_dir =
-      Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+      Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
 
     /* download */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_scala.scala
--- a/src/Pure/Admin/build_scala.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_scala.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -64,7 +64,7 @@
 
     val component_name = main_download.name + "-" + main_download.version
     val component_dir =
-      Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+      Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
 
     /* download */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_spass.scala
--- a/src/Pure/Admin/build_spass.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_spass.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -52,7 +52,7 @@
       }
 
       val component_dir =
-        Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+        Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
       val platform_name =
         proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_sqlite.scala
--- a/src/Pure/Admin/build_sqlite.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_sqlite.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -29,7 +29,7 @@
     /* component */
 
     val component_dir =
-      Components.Directory.create(target_dir + Path.basic(download_name), progress = progress)
+      Components.Directory(target_dir + Path.basic(download_name)).create(progress = progress)
 
 
     /* README */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_vampire.scala
--- a/src/Pure/Admin/build_vampire.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_vampire.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -47,7 +47,7 @@
 
       val component = proper_string(component_name) getOrElse make_component_name(version)
       val component_dir =
-        Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+        Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
 
       /* platform */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_verit.scala
--- a/src/Pure/Admin/build_verit.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_verit.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -42,7 +42,7 @@
 
       val component_name = "verit-" + version
       val component_dir =
-        Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+        Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
 
       /* platform */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_zipperposition.scala
--- a/src/Pure/Admin/build_zipperposition.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_zipperposition.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -27,7 +27,7 @@
 
       val component_name = "zipperposition-" + version
       val component_dir =
-        Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+        Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
 
       /* platform */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/Admin/build_zstd.scala
--- a/src/Pure/Admin/build_zstd.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/Admin/build_zstd.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -44,7 +44,7 @@
 
     val component_name = "zstd-jni-" + version
     val component_dir =
-      Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+      Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
     File.write(component_dir.README,
       "This is " + component_name + " from\n" + download_url +
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Pure/System/components.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -104,14 +104,6 @@
 
   object Directory {
     def apply(path: Path): Directory = new Directory(path.absolute)
-
-    def create(path: Path, progress: Progress = new Progress): Directory = {
-      val component_dir = new Directory(path.absolute)
-      progress.echo("Creating component directory " + component_dir.path)
-      Isabelle_System.new_directory(component_dir.path)
-      Isabelle_System.make_directory(component_dir.etc)
-      component_dir
-    }
   }
 
   class Directory private(val path: Path) {
@@ -126,6 +118,13 @@
     def README: Path = path + Path.basic("README")
     def LICENSE: Path = path + Path.basic("LICENSE")
 
+    def create(progress: Progress = new Progress): Directory = {
+      progress.echo("Creating component directory " + path)
+      Isabelle_System.new_directory(path)
+      Isabelle_System.make_directory(etc)
+      this
+    }
+
     def check: Boolean = settings.is_file || components.is_file
 
     def read_components(): List[String] =
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Tools/VSCode/src/build_vscode_extension.scala
--- a/src/Tools/VSCode/src/build_vscode_extension.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -151,7 +151,7 @@
 
     val component_name = "vscode_extension-" + Date.Format.alt_date(Date.now())
     val component_dir =
-      Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+      Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
 
     /* build */
diff -r 88cecb9f1cdc -r 9fe5d8c70352 src/Tools/VSCode/src/build_vscodium.scala
--- a/src/Tools/VSCode/src/build_vscodium.scala	Wed Nov 30 21:36:06 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscodium.scala	Wed Nov 30 21:53:55 2022 +0100
@@ -315,7 +315,7 @@
 
     val component_name = "vscodium-" + version
     val component_dir =
-      Components.Directory.create(target_dir + Path.explode(component_name), progress = progress)
+      Components.Directory(target_dir + Path.explode(component_name)).create(progress = progress)
 
 
     /* patches */