--- a/src/Pure/Isar/parse_spec.ML Fri Oct 04 13:22:35 2024 +0200
+++ b/src/Pure/Isar/parse_spec.ML Fri Oct 04 13:29:33 2024 +0200
@@ -17,6 +17,7 @@
val specification:
((binding * string option * mixfix) list * Specification.multi_specs_cmd) parser
val constdecl: (binding * string option * mixfix) parser
+ val bundles: (xstring * Position.T) list parser
val includes: (xstring * Position.T) list parser
val opening: (xstring * Position.T) list parser
val locale_fixes: (binding * string option * mixfix) list parser
@@ -81,11 +82,16 @@
>> Scan.triple2;
-(* locale and context elements *)
+(* bundles *)
+
+val bundles = Parse.and_list1 Parse.name_position;
-val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 Parse.name_position);
+val includes = Parse.$$$ "includes" |-- Parse.!!! bundles;
-val opening = Parse.$$$ "opening" |-- Parse.!!! (Scan.repeat1 Parse.name_position);
+val opening = Parse.$$$ "opening" |-- Parse.!!! bundles;
+
+
+(* locale and context elements *)
val locale_fixes =
Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix