changeset 75987 | ff2e67d73592 |
parent 75405 | b13ab7d11b90 |
child 76613 | b945e30b7471 |
--- a/src/Pure/Isar/parse.scala Fri Aug 26 21:28:26 2022 +0200 +++ b/src/Pure/Isar/parse.scala Fri Aug 26 21:34:09 2022 +0200 @@ -71,6 +71,7 @@ def path: Parser[String] = atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content)) + def chapter_name: Parser[String] = atom("chapter name", _.is_system_name) def session_name: Parser[String] = atom("session name", _.is_system_name) def theory_name: Parser[String] = atom("theory name", _.is_system_name)