# HG changeset patch
# User wenzelm
# Date 1661510646 -7200
# Node ID 75b65c1f7a1f8c6b3843ce94188305a0e9dd9b85
# Parent  34dd96a06c45ce7f7a5ef7be4c4d97c1902e7b79
tuned signature;

diff -r 34dd96a06c45 -r 75b65c1f7a1f src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Aug 26 12:38:00 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Aug 26 12:44:06 2022 +0200
@@ -883,7 +883,7 @@
       (EXPORT_CLASSPATH, Keyword.QUASI_COMMAND)
 
   abstract class Entry
-  sealed case class Chapter(name: String) extends Entry
+  sealed case class Chapter_Entry(name: String) extends Entry
   sealed case class Session_Entry(
     pos: Position.T,
     name: String,
@@ -907,10 +907,10 @@
   }
 
   private object Parsers extends Options.Parsers {
-    private val chapter: Parser[Chapter] = {
+    private val chapter: Parser[Chapter_Entry] = {
       val chapter_name = atom("chapter name", _.is_name)
 
-      command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
+      command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(a) }
     }
 
     private val session_entry: Parser[Session_Entry] = {
@@ -986,7 +986,7 @@
     var entry_chapter = UNSORTED
     val infos = new mutable.ListBuffer[Info]
     parse_root(path).foreach {
-      case Chapter(name) => entry_chapter = name
+      case Chapter_Entry(name) => entry_chapter = name
       case entry: Session_Entry =>
         infos += make_info(options, select, path.dir, entry_chapter, entry)
     }