src/Pure/Isar/parse.ML
changeset 75986 27d98da31985
parent 74887 56247fdb8bbb
child 76614 ac08b6e3b9e3
--- a/src/Pure/Isar/parse.ML	Fri Aug 26 21:25:35 2022 +0200
+++ b/src/Pure/Isar/parse.ML	Fri Aug 26 21:28:26 2022 +0200
@@ -72,6 +72,7 @@
   val path_input: Input.source parser
   val path: string parser
   val path_binding: (string * Position.T) parser
+  val chapter_name: (string * Position.T) parser
   val session_name: (string * Position.T) parser
   val theory_name: (string * Position.T) parser
   val liberal_name: string parser
@@ -289,6 +290,7 @@
 val path = path_input >> Input.string_of;
 val path_binding = group (fn () => "path binding (strict file name)") (position embedded);
 
+val chapter_name = group (fn () => "chapter name") name_position;
 val session_name = group (fn () => "session name") name_position;
 val theory_name = group (fn () => "theory name") name_position;