src/Pure/Thy/sessions.ML
changeset 76005 a9bbf075f431
parent 75998 c36e5c6f3069
child 76614 ac08b6e3b9e3
--- a/src/Pure/Thy/sessions.ML	Sat Aug 27 17:11:39 2022 +0200
+++ b/src/Pure/Thy/sessions.ML	Sat Aug 27 17:46:58 2022 +0200
@@ -20,6 +20,9 @@
 
 local
 
+val groups =
+  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [];
+
 val description =
   Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.embedded)) Input.empty;
 
@@ -54,7 +57,7 @@
 in
 
 val chapter_definition_parser =
-  Parse.chapter_name -- description >> (fn (_, descr) =>
+  Parse.chapter_name -- groups -- description >> (fn (_, descr) =>
     Toplevel.keep (fn state =>
       let
         val ctxt = Toplevel.context_of state;
@@ -65,8 +68,7 @@
       in () end));
 
 val session_parser =
-  Parse.session_name --
-  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] --
+  Parse.session_name -- groups --
   Scan.optional (Parse.$$$ "in" |-- Parse.!!! Parse.path_input) (Input.string ".") --
   (Parse.$$$ "=" |--
     Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) -- description --