src/Pure/Admin/component_hugo.scala
changeset 79975 90f4319c8b4f
parent 79974 f0150bc6fea5
--- a/src/Pure/Admin/component_hugo.scala	Sun Mar 24 15:05:22 2024 +0100
+++ b/src/Pure/Admin/component_hugo.scala	Sun Mar 24 15:13:35 2024 +0100
@@ -17,7 +17,8 @@
     override def toString: String = platform_name
 
     def is_windows: Boolean = url_template.contains("windows")
-    def url(base_url: String, version: String): String =
+
+    def download(base_url: String, version: String): String =
       base_url + "/v" + version + "/" + url_template.replace("{V}", version)
   }
 
@@ -53,8 +54,10 @@
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform.platform_name))
 
-      val url = platform.url(base_url, version)
-      val name = Library.take_suffix(_ != '/', url.toList)._2.mkString
+      val download = platform.download(base_url, version)
+      val name =
+        Url.get_base_name(download) getOrElse
+          error("Malformed download name " + quote(download))
 
       val exe = Path.basic("hugo").exe_if(platform.is_windows)
 
@@ -62,7 +65,7 @@
         Isabelle_System.with_tmp_dir("tmp", component_dir.path.file) { tmp_dir =>
           val archive_file = download_dir + Path.basic(name)
 
-          Isabelle_System.download_file(url, archive_file, progress = progress)
+          Isabelle_System.download_file(download, archive_file, progress = progress)
           Isabelle_System.extract(archive_file, tmp_dir)
           Isabelle_System.move_file(tmp_dir + exe, platform_dir)
           Isabelle_System.move_file(tmp_dir + Path.basic("LICENSE"), component_dir.LICENSE)
@@ -82,11 +85,11 @@
     /* README */
 
     File.write(component_dir.README,
-      """This Isabelle components provides a hugo extended """ + version + """.
+      """This Isabelle components provides hugo extended """ + version + """.
 
 See also https://gohugo.io and executables from """ + base_url + """
 
-        Fabian
+        Fabian Huch
         """ + Date.Format.date(Date.now()) + "\n")
   }