# HG changeset patch
# User wenzelm
# Date 1639151742 -3600
# Node ID 246e220681413a9cf2abbe3e1c48042df43443a5
# Parent  d969474ddc459fa142c651caee5060e7249bf2a1
clarified signature;

diff -r d969474ddc45 -r 246e22068141 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri Dec 10 08:58:09 2021 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri Dec 10 16:55:42 2021 +0100
@@ -75,8 +75,8 @@
   val mailman_archives: Logger_Task =
     Logger_Task("mailman_archives", logger =>
       {
-        Mailman.isabelle_users.download(mailman_archives_dir)
-        Mailman.isabelle_dev.download(mailman_archives_dir)
+        Mailman.isabelle_users.download_text(mailman_archives_dir)
+        Mailman.isabelle_dev.download_text(mailman_archives_dir)
       })
 
 
diff -r d969474ddc45 -r 246e22068141 src/Pure/General/mailman.scala
--- a/src/Pure/General/mailman.scala	Fri Dec 10 08:58:09 2021 +0100
+++ b/src/Pure/General/mailman.scala	Fri Dec 10 16:55:42 2021 +0100
@@ -16,27 +16,29 @@
 
   def archive(url: URL, name: String = ""): Archive =
   {
-    val text = Url.read(url)
-    val hrefs = """href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(text).map(_.group(1)).toList
+    val html = Url.read(url)
     val title =
-      """<title>The ([^</>]*) Archives</title>""".r.findFirstMatchIn(text).map(_.group(1))
+      """<title>The ([^</>]*) Archives</title>""".r.findFirstMatchIn(html).map(_.group(1))
+    val hrefs_text =
+      """href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(html).map(_.group(1)).toList
+
     val list_url =
       Url(Library.take_suffix[Char](_ == '/', Url.trim_index(url).toString.toList)._1.mkString + "/")
     val list_name =
       (proper_string(name) orElse title).getOrElse(error("Failed to determine mailing list name"))
-    new Archive(list_url, list_name, hrefs)
+    new Archive(list_url, list_name, hrefs_text)
   }
 
-  class Archive private[Mailman](val list_url: URL, val list_name: String, hrefs: List[String])
+  class Archive private[Mailman](val list_url: URL, val list_name: String, hrefs_text: List[String])
   {
     override def toString: String = list_name
 
-    def download(target_dir: Path, progress: Progress = new Progress): List[Path] =
+    def download_text(target_dir: Path, progress: Progress = new Progress): List[Path] =
     {
       val dir = target_dir + Path.basic(list_name)
       Isabelle_System.make_directory(dir)
 
-      hrefs.flatMap(name =>
+      hrefs_text.flatMap(name =>
         {
           val path = dir + Path.basic(name)
           val url = new URL(list_url, name)