src/Pure/Admin/component_javamail.scala
author Fabian Huch <huch@in.tum.de>
Tue, 09 Jan 2024 17:35:56 +0100
changeset 79443 0d7c7fe65638
parent 78827 06f0e720b913
permissions -rw-r--r--
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
78827
06f0e720b913 added component for javax mail;
Fabian Huch <huch@in.tum.de>
parents: 77619
diff changeset
     1
/*  Title:      Pure/Admin/component_javamail.scala
06f0e720b913 added component for javax mail;
Fabian Huch <huch@in.tum.de>
parents: 77619
diff 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: 78827
diff 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: 78827
diff 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: 78827
diff changeset
     6
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff 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: 78827
diff 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: 77619
diff changeset
     9
79443
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff 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: 78827
diff 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: 78827
diff changeset
    12
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff 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: 78827
diff 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: 78827
diff changeset
    15
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff 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: 78827
diff 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: 77619
diff 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: 78827
diff changeset
    24
  /* jars */
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff changeset
    25
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff 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: 78827
diff 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: 78827
diff changeset
    28
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff 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: 78827
diff 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: 78827
diff 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: 78827
diff changeset
    32
  }
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff changeset
    33
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff changeset
    34
  val jars =
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff changeset
    35
    List(
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff changeset
    36
      Jar("jakarta.mail", "jakarta.mail-api", "2.1.2"),
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff changeset
    37
      Jar("jakarta.activation", "jakarta.activation-api", "2.1.2"),
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff changeset
    38
      Jar("org.eclipse.angus", "angus-mail", "2.0.2"),
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff changeset
    39
      Jar("org.eclipse.angus", "angus-activation", "2.0.1"))
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff changeset
    40
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff changeset
    41
78827
06f0e720b913 added component for javax mail;
Fabian Huch <huch@in.tum.de>
parents: 77619
diff 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: 78827
diff 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: 77619
diff 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: 78827
diff 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: 78827
diff 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: 77619
diff 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: 78827
diff 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: 78827
diff 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: 78827
diff changeset
    64
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff changeset
    65
See also:
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff 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: 78827
diff 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: 78827
diff changeset
    68
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff 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: 78827
diff 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: 78827
diff changeset
    71
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff 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: 78827
diff 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: 78827
diff changeset
    74
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff 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: 78827
diff 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: 78827
diff changeset
    77
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff changeset
    78
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff changeset
    79
Fabian
0d7c7fe65638 update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents: 78827
diff 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: 78827
diff 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: 78827
diff 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: 78827
diff 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: 78827
diff 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: 78827
diff 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: 78827
diff 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: 78827
diff 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: 78827
diff 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: 77619
diff 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: 78827
diff 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: 77619
diff 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: 78827
diff 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: 78827
diff 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: 78827
diff 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: 78827
diff 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: 78827
diff 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
}