more robust, more strict;
authorwenzelm
Sat, 27 Aug 2022 12:04:49 +0200
changeset 75997 90ff9ed0cd75
parent 75996 633f74e679f5
child 75998 c36e5c6f3069
more robust, more strict;
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))
       }
   }