# HG changeset patch
# User wenzelm
# Date 1661594689 -7200
# Node ID 90ff9ed0cd7563ddad6aeebea0aac785076f79bf
# Parent  633f74e679f529c477bd9e381e3414f9f22f2a0d
more robust, more strict;

diff -r 633f74e679f5 -r 90ff9ed0cd75 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Aug 27 12:01:27 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 27 12:04:49 2022 +0200
@@ -923,14 +923,11 @@
       rev_list.find(_.name == chapter)
 
     def + (entry: Chapter_Def): Chapter_Defs =
-      if (entry.description.isEmpty) this
-      else {
-        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))
-        }
+      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))
       }
   }