# HG changeset patch
# User wenzelm
# Date 1661594487 -7200
# Node ID 633f74e679f529c477bd9e381e3414f9f22f2a0d
# Parent  627a08637c35c04fda099e682a6cf2a2be1cb404
tuned signature;

diff -r 627a08637c35 -r 633f74e679f5 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Aug 27 11:58:05 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 27 12:01:27 2022 +0200
@@ -919,23 +919,17 @@
     override def toString: String =
       list.map(_.name).mkString("Chapter_Defs(", ", ", ")")
 
-    private def find(chapter: String): Option[Chapter_Def] =
+    def get(chapter: String): Option[Chapter_Def] =
       rev_list.find(_.name == chapter)
 
-    def apply(chapter: String): String =
-      find(chapter) match {
-        case None => ""
-        case Some(ch_def) => ch_def.description
-      }
-
-    def + (ch_def: Chapter_Def): Chapter_Defs =
-      if (ch_def.description.isEmpty) this
+    def + (entry: Chapter_Def): Chapter_Defs =
+      if (entry.description.isEmpty) this
       else {
-        find(ch_def.name) match {
-          case None => new Chapter_Defs(ch_def :: rev_list)
-          case Some(old_def) =>
-            error("Duplicate chapter definition " + quote(ch_def.name) +
-              Position.here(old_def.pos) + Position.here(ch_def.pos))
+        get(entry.name) match {
+          case None => new Chapter_Defs(entry :: rev_list)
+          case Some(old_entry) =>
+            error("Duplicate chapter definition " + quote(entry.name) +
+              Position.here(old_entry.pos) + Position.here(entry.pos))
         }
       }
   }