clarified signature;

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

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

--- a/src/Pure/Thy/sessions.ML	Sat Dec 10 15:57:21 2022 +0100
+++ b/src/Pure/Thy/sessions.ML	Sat Dec 10 20:31:47 2022 +0100
@@ -31,22 +31,19 @@
 val theories =
   Parse.$$$ "theories" |-- Parse.!!! (Scan.optional Parse.options [] -- Scan.repeat1 theory_entry);
 
-val in_path =
-  Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.path_input --| Parse.$$$ ")");
-
 val document_theories =
   Parse.$$$ "document_theories" |-- Scan.repeat1 (Parse.input Parse.theory_name);
 
 val document_files =
   Parse.$$$ "document_files" |--
-    Parse.!!! (Scan.optional in_path (Input.string "document") -- Scan.repeat1 Parse.path_input);
+    Parse.!!! (Parse.in_path_parens "document" -- Scan.repeat1 Parse.path_input);
 
 val prune =
   Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.nat --| Parse.$$$ "]")) 0;
 
 val export_files =
   Parse.$$$ "export_files" |--
-    Parse.!!! (Scan.optional in_path (Input.string "export") -- prune -- Scan.repeat1 Parse.embedded);
+    Parse.!!! (Parse.in_path_parens "export" -- prune -- Scan.repeat1 Parse.embedded);
 
 val export_classpath =
   Parse.$$$ "export_classpath" |-- Scan.repeat Parse.embedded;
@@ -68,8 +65,7 @@
       in () end));
 
 val session_parser =
-  Parse.session_name -- groups --
-  Scan.optional (Parse.$$$ "in" |-- Parse.!!! Parse.path_input) (Input.string ".") --
+  Parse.session_name -- groups -- Parse.in_path "." --
   (Parse.$$$ "=" |--
     Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) -- description --
       Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --

--- a/src/Pure/Thy/sessions.scala	Sat Dec 10 15:57:21 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Dec 10 20:31:47 2022 +0100
@@ -893,7 +893,6 @@
   private val CHAPTER_DEFINITION = "chapter_definition"
   private val CHAPTER = "chapter"
   private val SESSION = "session"
-  private val IN = "in"
   private val DESCRIPTION = "description"
   private val DIRECTORIES = "directories"
   private val OPTIONS = "options"
@@ -906,8 +905,8 @@
   private val EXPORT_CLASSPATH = "export_classpath"
 
   val root_syntax: Outer_Syntax =
-    Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
-      GLOBAL + IN +
+    Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" + "in" +
+      GLOBAL +
       (CHAPTER_DEFINITION, Keyword.THY_DECL) +
       (CHAPTER, Keyword.THY_DECL) +
       (SESSION, Keyword.THY_DECL) +
@@ -1007,19 +1006,17 @@
           ((options | success(Nil)) ~ rep1(theory_entry)) ^^
           { case _ ~ (x ~ y) => (x, y) }
 
-      val in_path = $$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^ { case _ ~ (_ ~ x ~ _) => x }
-
       val document_theories =
         $$$(DOCUMENT_THEORIES) ~! rep1(position(name)) ^^ { case _ ~ x => x }
 
       val document_files =
-        $$$(DOCUMENT_FILES) ~!
-          ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
+        $$$(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 | success("export")) ~ prune ~ rep1(embedded)) ^^
+        $$$(EXPORT_FILES) ~! (in_path_parens("export") ~ prune ~ rep1(embedded)) ^^
           { case _ ~ (x ~ y ~ z) => (x, y, z) }
 
       val export_classpath =
@@ -1027,8 +1024,7 @@
           { case _ ~ x => x }
 
       command(SESSION) ~!
-        (position(session_name) ~ groups ~
-          (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
+        (position(session_name) ~ groups ~ in_path(".") ~
           ($$$("=") ~!
             (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~ description ~
               (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~