# HG changeset patch
# User wenzelm
# Date 1639512753 -3600
# Node ID f76bf7b5baed7859cbc1aefee06ca51f04a4ba68
# Parent  450597bdd2d3bdac206d1abd85af4fc31a682639
more accurate names;
complete coverage of mail addresses;

diff -r 450597bdd2d3 -r f76bf7b5baed src/Pure/General/mailman.scala
--- a/src/Pure/General/mailman.scala	Tue Dec 14 20:50:35 2021 +0100
+++ b/src/Pure/General/mailman.scala	Tue Dec 14 21:12:33 2021 +0100
@@ -30,6 +30,7 @@
       "Bisping, Benjamin" -> "Benjamin Bisping",
       "Blanchette, J.C." -> "Jasmin Christian Blanchette",
       "Buday Gergely István" -> "Gergely Buday",
+      "CALaF1UJ9Uy0vGCu4WkBmbfuPDxG7nFm8hfeCMP+O3g7_5CQ0Bw@mail.gmail.com" -> "",
       "CRACIUN F." -> "Florin Craciun",
       "Carsten Schuermann" -> "Carsten Schürmann",
       "Christoph Lueth" -> "Christoph Lüth",
@@ -43,6 +44,7 @@
       "Filip Maric" -> "Filip Marić",
       "Filip MariÄ" -> "Filip Marić",
       "Fleury Mathias" -> "Mathias Fleury",
+      "Francisco Jose Chaves Alonso" -> "Francisco Jose CHAVES ALONSO",
       "George K." -> "George Karabotsos",
       "Gidon ERNST" -> "Gidon Ernst",
       "Hans-JÃrg Schurr" -> "Hans-Jörg Schurr",
@@ -88,7 +90,6 @@
       "Stüber, Sebastian" -> "Sebastian Stüber",
       "Thiemann, Rene" -> "René Thiemann",
       "Thiemann, René" -> "René Thiemann",
-      "Thiemann, René" -> "René Thiemann",
       "Thomas Goethel" -> "Thomas Göthel",
       "Thomas.Sewell@data61.csiro.au" -> "tals4@cam.ac.uk",
       "Toby.Murray@data61.csiro.au" -> "toby.murray@unimelb.edu.au",
@@ -488,15 +489,18 @@
           HTML.input(message_match(head, """<li><em>Subject</em>:\s*(.*)</li>""".r)
             .getOrElse(err("Missing Subject")).group(1)))
 
+      def parse_author_info(re: Regex): List[String] =
+        message_match(head, re) match {
+          case None => Nil
+          case Some(m) => Address.parse(m.group(1)).map(a => HTML.input(make_name(a)))
+        }
+
       val author_info =
-        message_match(head, """<li><em>From</em>:\s*(.*?)\s*</li>""".r) match {
-          case None => err("Missing From")
-          case Some(m) =>
-            val res =
-              Address.parse(m.group(1)).map(a => HTML.input(make_name(a)))
-                .distinct.filter(_.nonEmpty)
-            if (res.nonEmpty) res else err("Malformed author information")
-        }
+        (parse_author_info("""<li><em>From</em>:\s*(.*?)\s*</li>""".r) :::
+          parse_author_info("""<li><em>Reply-to</em>:\s*(.*?)\s*</li>""".r))
+        .distinct.filter(_.nonEmpty)
+
+      if (author_info.isEmpty) err("Malformed author information")
 
       val tags = List(list_name)
 
@@ -520,12 +524,6 @@
       def unapply(s: String): Option[Date] = Format.unapply(s.replaceAll("""\s+""", " "))
     }
 
-    override def make_name(str: String): String =
-    {
-      val s = Library.perhaps_unsuffix(" via RT", super.make_name(str))
-      if (s == "sys-admin@cl.cam.ac.uk") "" else s
-    }
-
     override def message_content(name: String, lines: List[String]): Message =
     {
       def err(msg: String = ""): Nothing =