tuned output: proper progress;
authorwenzelm
Sun, 19 Jan 2025 15:36:12 +0100
changeset 81927 d59262da07ac
parent 81926 402660d4558e
child 81928 d6366c0c9d5c
tuned output: proper progress;
src/Pure/Admin/component_hol_light.scala
src/Pure/Admin/component_polyml.scala
--- a/src/Pure/Admin/component_hol_light.scala	Sun Jan 19 15:13:42 2025 +0100
+++ b/src/Pure/Admin/component_hol_light.scala	Sun Jan 19 15:36:12 2025 +0100
@@ -36,7 +36,8 @@
     /* component */
 
     val component_name = "hol_light_import-" + Date.Format.alt_date(Date.now())
-    val component_dir = Components.Directory(target_dir + Path.basic(component_name)).create()
+    val component_dir =
+      Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
     val platform = Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true, apple = true)
     val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic(platform))
--- a/src/Pure/Admin/component_polyml.scala	Sun Jan 19 15:13:42 2025 +0100
+++ b/src/Pure/Admin/component_polyml.scala	Sun Jan 19 15:36:12 2025 +0100
@@ -195,8 +195,8 @@
     /* component */
 
     val component_name1 = if (component_name.isEmpty) "polyml-" + polyml_version else component_name
-    val component_dir = Components.Directory(target_dir + Path.basic(component_name1)).create()
-    progress.echo("Component " + component_dir)
+    val component_dir =
+      Components.Directory(target_dir + Path.basic(component_name1)).create(progress = progress)
 
 
     /* download and build */