# HG changeset patch
# User wenzelm
# Date 1639473588 -3600
# Node ID f5ad3214bef425d4f8205d8939b0e229ee989b33
# Parent  0f27dcd030b8e31af24e07ddbaf42fe4d651503d
clarified signature: more operations;

diff -r 0f27dcd030b8 -r f5ad3214bef4 src/Pure/General/mailman.scala
--- a/src/Pure/General/mailman.scala	Tue Dec 14 10:07:10 2021 +0100
+++ b/src/Pure/General/mailman.scala	Tue Dec 14 10:19:48 2021 +0100
@@ -24,7 +24,8 @@
     title: String,
     author_name: String,
     author_address: String,
-    body: String)
+    body: String,
+    tags: List[String])
   {
     override def toString: String = name
     def print: String =
@@ -38,6 +39,16 @@
   {
     def apply(msgs: List[Message]): Messages =
       new Messages(msgs.sortBy(_.date)(Date.Ordering))
+
+    def find(dir: Path): Messages =
+    {
+      val msgs =
+        for {
+          archive <- List(Isabelle_Users, Isabelle_Dev)
+          msg <- archive.find_messages(dir + Path.basic(archive.list_name))
+        } yield msg
+      Messages(msgs)
+    }
   }
 
   class Messages private(val sorted: List[Message])
@@ -349,7 +360,9 @@
             (if (a == b) "" else a, b)
         }
 
-      Message(name, date, title, author_name, author_address, body)
+      val tags = List(list_name)
+
+      Message(name, date, title, author_name, author_address, body, tags)
     }
   }
 
@@ -407,7 +420,9 @@
             if (a == author_address) "" else a
         }
 
-      Message(name, date, title, author_name, author_address, body)
+      val tags = List(list_name)
+
+      Message(name, date, title, author_name, author_address, body, tags)
     }
   }
 }