changeset 75987 | ff2e67d73592 |
parent 75986 | 27d98da31985 |
child 75995 | 627a08637c35 |
--- a/src/Pure/Thy/sessions.scala Fri Aug 26 21:28:26 2022 +0200 +++ b/src/Pure/Thy/sessions.scala Fri Aug 26 21:34:09 2022 +0200 @@ -941,9 +941,6 @@ } private object Parsers extends Options.Parsers { - private val chapter_name: Parser[String] = - atom("chapter name", _.is_name) - private val chapter_def: Parser[Chapter_Def] = command(CHAPTER_DEFINITION) ~! (position(chapter_name) ~ $$$(DESCRIPTION) ~ text) ^^