# HG changeset patch
# User wenzelm
# Date 1661542449 -7200
# Node ID ff2e67d73592aba8999479b759eb2d623021ea3d
# Parent  27d98da31985231150f64bdf649c32cef9ed3014
more robust: proper system_name;

diff -r 27d98da31985 -r ff2e67d73592 src/Pure/Isar/parse.scala
--- 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)
 
diff -r 27d98da31985 -r ff2e67d73592 src/Pure/Thy/sessions.scala
--- 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) ^^