# HG changeset patch # User wenzelm # Date 1711289615 -3600 # Node ID 90f4319c8b4f95926703d972f437871685331d18 # Parent f0150bc6fea5bb9bb0dfa1555bc95e113d166389 misc tuning; diff -r f0150bc6fea5 -r 90f4319c8b4f src/Pure/Admin/component_hugo.scala --- 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") }