| author | Fabian Huch <huch@in.tum.de> | 
| Wed, 22 Oct 2025 10:31:50 +0200 | |
| changeset 83329 | a12f6d3bae26 | 
| parent 81901 | fab7c8c91c09 | 
| permissions | -rw-r--r-- | 
| 78827 
06f0e720b913
added component for javax mail;
 Fabian Huch <huch@in.tum.de> parents: 
77619diff
changeset | 1 | /* Title: Pure/Admin/component_javamail.scala | 
| 
06f0e720b913
added component for javax mail;
 Fabian Huch <huch@in.tum.de> parents: 
77619diff
changeset | 2 | Author: Fabian Huch, TU Muenchen | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 3 | |
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 4 | Build Isabelle java mail component (previously javax-mail, now jakarta + eclipse angus) | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 5 | from official downloads. See also: | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 6 | |
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 7 | - https://jakarta.ee/specifications/mail | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 8 | - https://mvnrepository.com/artifact/jakarta.mail/jakarta.mail-api | 
| 78827 
06f0e720b913
added component for javax mail;
 Fabian Huch <huch@in.tum.de> parents: 
77619diff
changeset | 9 | |
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 10 | - https://jakarta.ee/specifications/activation | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 11 | - https://mvnrepository.com/artifact/jakarta.activation/jakarta.activation-api | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 12 | |
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 13 | - https://eclipse-ee4j.github.io/angus-mail/ | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 14 | - https://mvnrepository.com/artifact/org.eclipse.angus/angus-mail | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 15 | |
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 16 | - https://eclipse-ee4j.github.io/angus-activation/ | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 17 | - https://mvnrepository.com/artifact/org.eclipse.angus/angus-activation | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 18 | */ | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 19 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 20 | package isabelle | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 21 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 22 | |
| 78827 
06f0e720b913
added component for javax mail;
 Fabian Huch <huch@in.tum.de> parents: 
77619diff
changeset | 23 | object Component_Javamail {
 | 
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 24 | /* jars */ | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 25 | |
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 26 |   sealed case class Jar(group_id: String, artifact_id: String, version: String) {
 | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 27 | override def toString: String = group_id + ":" + artifact_id | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 28 | |
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 29 | def file_name: String = artifact_id + "-" + version + ".jar" | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 30 |     def maven_dir: String = group_id.replace('.', '/') + "/" + artifact_id + "/" + version
 | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 31 | def url(repo_url: String): String = repo_url + "/" + maven_dir + "/" + file_name | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 32 | } | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 33 | |
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 34 | val jars = | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 35 | List( | 
| 83329 
a12f6d3bae26
update to javamail-20251022;
 Fabian Huch <huch@in.tum.de> parents: 
81901diff
changeset | 36 |       Jar("jakarta.mail", "jakarta.mail-api", "2.1.5"),
 | 
| 
a12f6d3bae26
update to javamail-20251022;
 Fabian Huch <huch@in.tum.de> parents: 
81901diff
changeset | 37 |       Jar("jakarta.activation", "jakarta.activation-api", "2.1.4"),
 | 
| 
a12f6d3bae26
update to javamail-20251022;
 Fabian Huch <huch@in.tum.de> parents: 
81901diff
changeset | 38 |       Jar("org.eclipse.angus", "angus-mail", "2.0.5"),
 | 
| 
a12f6d3bae26
update to javamail-20251022;
 Fabian Huch <huch@in.tum.de> parents: 
81901diff
changeset | 39 |       Jar("org.eclipse.angus", "angus-activation", "2.0.3"))
 | 
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 40 | |
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 41 | |
| 78827 
06f0e720b913
added component for javax mail;
 Fabian Huch <huch@in.tum.de> parents: 
77619diff
changeset | 42 | /* build javamail */ | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 43 | |
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 44 | val default_download_repo = "https://repo1.maven.org/maven2" | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 45 | |
| 78827 
06f0e720b913
added component for javax mail;
 Fabian Huch <huch@in.tum.de> parents: 
77619diff
changeset | 46 | def build_javamail( | 
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 47 | download_repo: String = default_download_repo, | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 48 | progress: Progress = new Progress, | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 49 | target_dir: Path = Path.current | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 50 |   ): Unit = {
 | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 51 | /* component */ | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 52 | |
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 53 | val component_name = "javamail-" + Date.Format.alt_date(Date.now()) | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 54 | val component_dir = | 
| 78827 
06f0e720b913
added component for javax mail;
 Fabian Huch <huch@in.tum.de> parents: 
77619diff
changeset | 55 | Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress) | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 56 | |
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 57 | File.write(component_dir.LICENSE, "See the file META-INF/LICENSE.txt in each jar file.") | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 58 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 59 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 60 | /* README */ | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 61 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 62 | File.write(component_dir.README, | 
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 63 | "This is " + component_name + " from\n" + download_repo + """ | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 64 | |
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 65 | See also: | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 66 | - https://jakarta.ee/specifications/mail | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 67 | - https://mvnrepository.com/artifact/jakarta.mail/jakarta.mail-api | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 68 | |
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 69 | - https://jakarta.ee/specifications/activation | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 70 | - https://mvnrepository.com/artifact/jakarta.activation/jakarta.activation-api | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 71 | |
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 72 | - https://eclipse-ee4j.github.io/angus-mail/ | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 73 | - https://mvnrepository.com/artifact/org.eclipse.angus/angus-mail | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 74 | |
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 75 | - https://eclipse-ee4j.github.io/angus-activation/ | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 76 | - https://mvnrepository.com/artifact/org.eclipse.angus/angus-activation | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 77 | |
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 78 | |
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 79 | Fabian | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 80 | """ + Date.Format.date(Date.now()) + "\n") | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 81 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 82 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 83 | /* settings */ | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 84 | |
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 85 | val settings = jars.map(jar => "\nclasspath \"$COMPONENT/lib/" + jar.file_name + "\"") | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 86 | component_dir.write_settings(settings.mkString) | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 87 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 88 | |
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 89 | /* jars */ | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 90 | |
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 91 | Isabelle_System.make_directory(component_dir.lib) | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 92 |     for (jar <- jars) {
 | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 93 | val path = component_dir.lib + Path.basic(jar.file_name) | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 94 | Isabelle_System.download_file(jar.url(download_repo), path, progress = progress) | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 95 | } | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 96 | } | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 97 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 98 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 99 | /* Isabelle tool wrapper */ | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 100 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 101 | val isabelle_tool = | 
| 78827 
06f0e720b913
added component for javax mail;
 Fabian Huch <huch@in.tum.de> parents: 
77619diff
changeset | 102 |     Isabelle_Tool("component_javamail", "build Isabelle javamail component from official download",
 | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 103 | Scala_Project.here, | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 104 |       { args =>
 | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 105 | var target_dir = Path.current | 
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 106 | var download_repo = default_download_repo | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 107 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 108 |         val getopts = Getopts("""
 | 
| 78827 
06f0e720b913
added component for javax mail;
 Fabian Huch <huch@in.tum.de> parents: 
77619diff
changeset | 109 | Usage: isabelle component_javamail [OPTIONS] DOWNLOAD | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 110 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 111 | Options are: | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 112 | -D DIR target directory (default ".") | 
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 113 | -U URL download repository URL | 
| 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 114 | (default: """" + default_download_repo + """") | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 115 | |
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 116 | Build javamail component from the specified download repository (maven). | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 117 | """, | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 118 | "D:" -> (arg => target_dir = Path.explode(arg)), | 
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 119 | "U:" -> (arg => download_repo = arg)) | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 120 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 121 | val more_args = getopts(args) | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 122 | if (more_args.nonEmpty) getopts.usage() | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 123 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 124 | val progress = new Console_Progress() | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 125 | |
| 79443 
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
 Fabian Huch <huch@in.tum.de> parents: 
78827diff
changeset | 126 | build_javamail(download_repo = download_repo, progress = progress, target_dir = target_dir) | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 127 | }) | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 128 | } |