diff -r 987cd5e21f72 -r b9715600883c src/Pure/Build/sessions.scala --- a/src/Pure/Build/sessions.scala Thu Aug 14 14:25:20 2025 +0100 +++ b/src/Pure/Build/sessions.scala Sat Aug 16 12:50:32 2025 +0200 @@ -1185,6 +1185,12 @@ private val chapter_entry: Parser[Chapter_Entry] = command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(a) } + private val prune: Parser[Int] = + $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0) + + private val export_files_args: Parser[(String, Int, List[String])] = + in_path_parens("export") ~ prune ~ rep1(embedded) ^^ { case x ~ y ~ z => (x, y, z) } + private val session_entry: Parser[Session_Entry] = { val options = $$$("[") ~> rep1sep(option_spec, $$$(",")) <~ $$$("]") @@ -1203,11 +1209,8 @@ $$$(DOCUMENT_FILES) ~! (in_path_parens("document") ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) } - val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0) - val export_files = - $$$(EXPORT_FILES) ~! (in_path_parens("export") ~ prune ~ rep1(embedded)) ^^ - { case _ ~ (x ~ y ~ z) => (x, y, z) } + $$$(EXPORT_FILES) ~! export_files_args ^^ { case _ ~ x => x } val export_classpath = $$$(EXPORT_CLASSPATH) ~! (rep1(embedded) | success(List("*:classpath/*.jar"))) ^^ @@ -1240,6 +1243,14 @@ case bad => error(bad.toString) } } + + def parse_exports(str: String, start: Token.Pos): (String, Int, List[String]) = { + val toks = Token.explode(root_syntax.keywords, str) + parse_all(export_files_args, Token.reader(toks, start)) match { + case Success(result, _) => result + case bad => error(bad.toString) + } + } } def parse_root(path: Path): List[Entry] = Parsers.parse_root(path) @@ -1254,6 +1265,9 @@ } yield line } + def parse_exports(str: String, start: Token.Pos = Token.Pos.none): (String, Int, List[String]) = + Parsers.parse_exports(str, start) + /* load sessions from certain directories */