--- a/src/Pure/Isar/parse.scala Sat Dec 10 15:57:21 2022 +0100
+++ b/src/Pure/Isar/parse.scala Sat Dec 10 20:31:47 2022 +0100
@@ -71,6 +71,12 @@
def path: Parser[String] =
atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content))
+ def in_path(default: String): Parser[String] =
+ $$$("in") ~! path ^^ { case _ ~ x => x } | success(default)
+
+ def in_path_parens(default: String): Parser[String] =
+ $$$("(") ~! ($$$("in") ~ path ~ $$$(")")) ^^ { case _ ~ (_ ~ x ~ _) => x } | success(default)
+
def chapter_name: Parser[String] = atom("chapter name", _.is_system_name)
def session_name: Parser[String] = atom("session name", _.is_system_name)
def theory_name: Parser[String] = atom("theory name", _.is_system_name)