# HG changeset patch
# User wenzelm
# Date 1639472034 -3600
# Node ID 1c75f42770b57fbe24bc1d8ff8de85ec11b85fe8
# Parent  1753dade9a24d27e3d7c50385353c63763abf5ae
tuned;

diff -r 1753dade9a24 -r 1c75f42770b5 src/Pure/General/mailman.scala
--- a/src/Pure/General/mailman.scala	Tue Dec 14 09:46:29 2021 +0100
+++ b/src/Pure/General/mailman.scala	Tue Dec 14 09:53:54 2021 +0100
@@ -34,37 +34,6 @@
     def normal_address: String = Word.lowercase(author_address)
   }
 
-  private class Message_Chunk(bg: String = "", en: String = "")
-  {
-    def unapply(lines: List[String]): Option[List[String]] =
-    {
-      val res1 =
-        if (bg.isEmpty) Some(lines)
-        else {
-          lines.dropWhile(_ != bg) match {
-            case Nil => None
-            case _ :: rest => Some(rest)
-          }
-        }
-      if (en.isEmpty) res1
-      else {
-        res1 match {
-          case None => None
-          case Some(lines1) =>
-            val lines2 = lines1.takeWhile(_ != en)
-            if (lines1.drop(lines2.length).isEmpty) None else Some(lines2)
-        }
-      }
-    }
-
-    def get(lines: List[String]): List[String] =
-      unapply(lines) getOrElse
-        error("Missing delimiters:" +
-          (if (bg.nonEmpty) " " else "") + bg +
-          (if (en.nonEmpty) " " else "") + en)
-  }
-
-
   /* integrity check */
 
   def check_messages(msgs: List[Message]): Unit =
@@ -228,6 +197,36 @@
     }
   }
 
+  private class Message_Chunk(bg: String = "", en: String = "")
+  {
+    def unapply(lines: List[String]): Option[List[String]] =
+    {
+      val res1 =
+        if (bg.isEmpty) Some(lines)
+        else {
+          lines.dropWhile(_ != bg) match {
+            case Nil => None
+            case _ :: rest => Some(rest)
+          }
+        }
+      if (en.isEmpty) res1
+      else {
+        res1 match {
+          case None => None
+          case Some(lines1) =>
+            val lines2 = lines1.takeWhile(_ != en)
+            if (lines1.drop(lines2.length).isEmpty) None else Some(lines2)
+        }
+      }
+    }
+
+    def get(lines: List[String]): List[String] =
+      unapply(lines) getOrElse
+        error("Missing delimiters:" +
+          (if (bg.nonEmpty) " " else "") + bg +
+          (if (en.nonEmpty) " " else "") + en)
+  }
+
 
   /* isabelle-users mailing list */