# HG changeset patch
# User wenzelm
# Date 1639419684 -3600
# Node ID e0070487b6350278bd6f12662b47ed391c824d49
# Parent  15404e37c12793b35614383e003fd69befdedcbc
clarified name;

diff -r 15404e37c127 -r e0070487b635 src/Pure/General/mailman.scala
--- a/src/Pure/General/mailman.scala	Mon Dec 13 17:59:02 2021 +0100
+++ b/src/Pure/General/mailman.scala	Mon Dec 13 19:21:24 2021 +0100
@@ -112,7 +112,7 @@
     tag: String = "")
   {
     def message_regex: Regex
-    def message_content(href: String, lines: List[String]): Message
+    def message_content(name: String, lines: List[String]): Message
 
     private val main_url: URL =
       Url(Library.take_suffix[Char](_ == '/', Url.trim_index(url).toString.toList)._1.mkString + "/")
@@ -127,6 +127,8 @@
     }
     override def toString: String = list_name
 
+    def full_name(href: String): String = list_name + "/" + href
+
     def list_tag: String = proper_string(tag).getOrElse(list_name)
 
     def read_text(href: String): String = Url.read(new URL(main_url, href))
@@ -200,7 +202,11 @@
       for {
         file <- File.find_files(dir.file, file => file.getName.endsWith(".html"))
         rel_path <- File.relative_path(dir, File.path(file))
-      } yield message_content(rel_path.implode, split_lines(File.read(file)))
+      }
+      yield {
+        val name = full_name(rel_path.implode)
+        message_content(name, split_lines(File.read(file)))
+      }
     }
   }
 
@@ -255,10 +261,10 @@
       }
     }
 
-    override def message_content(href: String, lines: List[String]): Message =
+    override def message_content(name: String, lines: List[String]): Message =
     {
       def err(msg: String = ""): Nothing =
-        error("Malformed message: " + href + (if (msg.isEmpty) "" else "\n" + msg))
+        error("Malformed message: " + name + (if (msg.isEmpty) "" else "\n" + msg))
 
       val (head, body) =
         try { (Head.get(lines), Body.get(lines)) }
@@ -284,7 +290,7 @@
         }
 
       Message(
-        href, date, trim_title(title),
+        name, date, trim_title(title),
         trim_name(proper_string(author_name) getOrElse author_address),
         author_address,
         cat_lines(body))
@@ -304,10 +310,10 @@
       def unapply(s: String): Option[Date] = Format.unapply(s.replaceAll("""\s+""", " "))
     }
 
-    override def message_content(href: String, lines: List[String]): Message =
+    override def message_content(name: String, lines: List[String]): Message =
     {
       def err(msg: String = ""): Nothing =
-        error("Malformed message: " + href + (if (msg.isEmpty) "" else "\n" + msg))
+        error("Malformed message: " + name + (if (msg.isEmpty) "" else "\n" + msg))
 
       val (head, body) =
         try { (Head.get(lines), Body.get(lines)) }
@@ -335,7 +341,7 @@
         }
 
       Message(
-        href, date, trim_title(title),
+        name, date, trim_title(title),
         trim_name(proper_string(author_name) getOrElse author_address),
         author_address,
         cat_lines(body))