--- 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 --