diff -r a7241e5db601 -r 0d7c7fe65638 src/Pure/Admin/component_javamail.scala --- a/src/Pure/Admin/component_javamail.scala Mon Jan 08 23:44:02 2024 +0100 +++ b/src/Pure/Admin/component_javamail.scala Tue Jan 09 17:35:56 2024 +0100 @@ -1,64 +1,98 @@ /* Title: Pure/Admin/component_javamail.scala Author: Fabian Huch, TU Muenchen -Build Isabelle javax-mail component from official download. See also: +Build Isabelle java mail component (previously javax-mail, now jakarta + eclipse angus) +from official downloads. See also: + + - https://jakarta.ee/specifications/mail + - https://mvnrepository.com/artifact/jakarta.mail/jakarta.mail-api - - https://javaee.github.io/javamail/ - - https://mvnrepository.com/artifact/javax.mail/mail + - https://jakarta.ee/specifications/activation + - https://mvnrepository.com/artifact/jakarta.activation/jakarta.activation-api + + - https://eclipse-ee4j.github.io/angus-mail/ + - https://mvnrepository.com/artifact/org.eclipse.angus/angus-mail + + - https://eclipse-ee4j.github.io/angus-activation/ + - https://mvnrepository.com/artifact/org.eclipse.angus/angus-activation */ package isabelle object Component_Javamail { + /* jars */ + + sealed case class Jar(group_id: String, artifact_id: String, version: String) { + override def toString: String = group_id + ":" + artifact_id + + def file_name: String = artifact_id + "-" + version + ".jar" + def maven_dir: String = group_id.replace('.', '/') + "/" + artifact_id + "/" + version + def url(repo_url: String): String = repo_url + "/" + maven_dir + "/" + file_name + } + + val jars = + List( + Jar("jakarta.mail", "jakarta.mail-api", "2.1.2"), + Jar("jakarta.activation", "jakarta.activation-api", "2.1.2"), + Jar("org.eclipse.angus", "angus-mail", "2.0.2"), + Jar("org.eclipse.angus", "angus-activation", "2.0.1")) + + /* build javamail */ - val default_download_url = - "https://repo1.maven.org/maven2/javax/mail/mail/1.4.7/mail-1.4.7.jar" + val default_download_repo = "https://repo1.maven.org/maven2" def build_javamail( - download_url: String = default_download_url, + download_repo: String = default_download_repo, progress: Progress = new Progress, target_dir: Path = Path.current ): Unit = { - val Download_Name = """^.*/([^/]+)\.jar""".r - val download_name = - download_url match { - case Download_Name(download_name) => download_name - case _ => error("Malformed jar download URL: " + quote(download_url)) - } - val component_name = "java" + download_name - - /* component */ + val component_name = "javamail-" + Date.Format.alt_date(Date.now()) val component_dir = Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress) - File.write(component_dir.LICENSE, - Url.read("https://raw.githubusercontent.com/javaee/javamail/master/LICENSE.txt")) + File.write(component_dir.LICENSE, "See the file META-INF/LICENSE.txt in each jar file.") /* README */ File.write(component_dir.README, - "This is " + component_name + " from\n" + download_url + - "\n\nSee also https://javaee.github.io/javamail and https://mvnrepository.com/artifact/javax.mail/mail" + - "\n\n Fabian\n " + Date.Format.date(Date.now()) + "\n") + "This is " + component_name + " from\n" + download_repo + """ + +See also: + - https://jakarta.ee/specifications/mail + - https://mvnrepository.com/artifact/jakarta.mail/jakarta.mail-api + + - https://jakarta.ee/specifications/activation + - https://mvnrepository.com/artifact/jakarta.activation/jakarta.activation-api + + - https://eclipse-ee4j.github.io/angus-mail/ + - https://mvnrepository.com/artifact/org.eclipse.angus/angus-mail + + - https://eclipse-ee4j.github.io/angus-activation/ + - https://mvnrepository.com/artifact/org.eclipse.angus/angus-activation + + +Fabian + """ + Date.Format.date(Date.now()) + "\n") /* settings */ - component_dir.write_settings(""" -classpath "$COMPONENT/lib/""" + download_name + """.jar" -""") + val settings = jars.map(jar => "\nclasspath \"$COMPONENT/lib/" + jar.file_name + "\"") + component_dir.write_settings(settings.mkString) - /* jar */ + /* jars */ - val jar = component_dir.lib + Path.basic(download_name).jar - Isabelle_System.make_directory(jar.dir) - Isabelle_System.download_file(download_url, jar, progress = progress) + Isabelle_System.make_directory(component_dir.lib) + for (jar <- jars) { + val path = component_dir.lib + Path.basic(jar.file_name) + Isabelle_System.download_file(jar.url(download_repo), path, progress = progress) + } } @@ -69,26 +103,26 @@ Scala_Project.here, { args => var target_dir = Path.current - var download_url = default_download_url + var download_repo = default_download_repo val getopts = Getopts(""" Usage: isabelle component_javamail [OPTIONS] DOWNLOAD Options are: -D DIR target directory (default ".") - -U URL download URL - (default: """" + default_download_url + """") + -U URL download repository URL + (default: """" + default_download_repo + """") - Build javamail component from the specified download URL (JAR). + Build javamail component from the specified download repository (maven). """, "D:" -> (arg => target_dir = Path.explode(arg)), - "U:" -> (arg => download_url = arg)) + "U:" -> (arg => download_repo = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() - build_javamail(download_url = download_url, progress = progress, target_dir = target_dir) + build_javamail(download_repo = download_repo, progress = progress, target_dir = target_dir) }) }