--- a/src/Pure/Isar/parse.ML Sat Dec 10 15:57:21 2022 +0100
+++ b/src/Pure/Isar/parse.ML Sat Dec 10 20:31:47 2022 +0100
@@ -72,6 +72,8 @@
val path_input: Input.source parser
val path: string parser
val path_binding: (string * Position.T) parser
+ val in_path: string -> Input.source parser
+ val in_path_parens: string -> Input.source parser
val chapter_name: (string * Position.T) parser
val session_name: (string * Position.T) parser
val theory_name: (string * Position.T) parser
@@ -290,6 +292,12 @@
val path = path_input >> Input.string_of;
val path_binding = group (fn () => "path binding (strict file name)") (position embedded);
+fun in_path default =
+ Scan.optional ($$$ "in" |-- !!! path_input) (Input.string default);
+
+fun in_path_parens default =
+ Scan.optional ($$$ "(" |-- !!! ($$$ "in" |-- path_input --| $$$ ")")) (Input.string default);
+
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;