support for "isabelle process_theories -E EXPORTS";

--- a/src/Doc/System/Environment.thy	Thu Aug 14 14:25:20 2025 +0100
+++ b/src/Doc/System/Environment.thy	Sat Aug 16 12:50:32 2025 +0200
@@ -305,10 +305,11 @@
 
 text \<open>
   The raw Isabelle ML process has limited use in actual applications: it lacks
-  the full session context that is required for Isabelle/ML/Scala integration
-  and Prover IDE messages or markup. It is better to use @{tool build}
-  (\secref{sec:tool-build}) for regular sessions, or its front-end @{tool
-  process_theories} (\secref{sec:tool-process-theories}) for adhoc sessions.
+  the full session context that is required for export artifacts,
+  Isabelle/ML/Scala integration and Prover IDE messages or markup. It is
+  better to use @{tool build} (\secref{sec:tool-build}) for regular sessions,
+  or its front-end @{tool process_theories}
+  (\secref{sec:tool-process-theories}) for adhoc sessions.
 \<close>
 
 

--- a/src/Doc/System/Sessions.thy	Thu Aug 14 14:25:20 2025 +0100
+++ b/src/Doc/System/Sessions.thy	Sat Aug 16 12:50:32 2025 +0200
@@ -1211,6 +1211,7 @@
 
   Options are:
     -D DIR       explicit session directory (default: private)
+    -E EXPORTS   write session export artifacts to file-system
     -F FILE      include additional session files, listed in FILE
     -H REGEX     filter messages by matching against head
     -M REGEX     filter messages by matching against body
@@ -1246,6 +1247,14 @@
   too.
 
   \<^medskip>
+  Option \<^verbatim>\<open>-E\<close> writes session export artifacts to the local file-system: it is
+  a combination of option \<^verbatim>\<open>-e\<close> from @{tool build}, together
+  \isakeyword{export_files} from session ROOT declarations
+  (\secref{sec:session-root}). The declaration syntax allows to specify an
+  explicit export directory, which is here understood as relative to the
+  current working directory. The default directory is ``\<^verbatim>\<open>export\<close>''.
+
+  \<^medskip>
   Option \<^verbatim>\<open>-l\<close> specifies the parent logic session, which is produced on the
   spot using @{tool build}. Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> work as in @{tool
   build}.
@@ -1276,6 +1285,11 @@
   of its original session context:
   @{verbatim [display] \<open>  isabelle process_theories -f '~~/src/HOL/Examples/Seq.thy'\<close>}
 
+  \<^medskip>
+  Process a theory with session export artifacts, stemming from the
+  Isabelle/HOL code generator (result directory ``\<^verbatim>\<open>code\<close>''):
+
+  @{verbatim [display] \<open>  isabelle process_theories -E '[1] "*:code/**"' HOL-Decision_Procs.Cooper\<close>}
 \<close>
 
 end

--- 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 */
 

--- a/src/Pure/Tools/process_theories.scala	Thu Aug 14 14:25:20 2025 +0100
+++ b/src/Pure/Tools/process_theories.scala	Sat Aug 16 12:50:32 2025 +0200
@@ -33,6 +33,7 @@
     breakgain: Double = Pretty.default_breakgain,
     metric: Pretty.Metric = Symbol.Metric,
     unicode_symbols: Boolean = false,
+    export_files: List[(String, Int, List[String])] = Nil,
     progress: Progress = new Progress
   ): Build.Results = {
     Isabelle_System.with_tmp_dir("private") { private_dir =>
@@ -99,7 +100,9 @@
         Sessions.Session_Entry(
           parent = Some(logic),
           theories = session_theories.map(a => (Nil, List(((a, Position.none), false)))),
-          imports = session_imports)
+          imports = session_imports,
+          export_files = export_files
+            .map({ case (a, b, c) => (Path.explode(a).absolute.implode, b, c) }))
 
       val session_info =
         Sessions.Info.make(session_entry, draft_session = true,
@@ -128,7 +131,8 @@
 
       Build.build(options, private_dir = Some(private_dir), dirs = dirs, progress = progress,
         infos = List(session_info), selection = Sessions.Selection.session(session_name),
-        session_setup = session_setup)
+        session_setup = session_setup,
+        export_files = export_files.nonEmpty)
     }
   }
 
@@ -141,6 +145,7 @@
     Scala_Project.here,
     { args =>
       var directory: Option[Path] = None
+      val export_files = new mutable.ListBuffer[(String, Int, List[String])]
       val message_head = new mutable.ListBuffer[Regex]
       val message_body = new mutable.ListBuffer[Regex]
       var output_messages = false
@@ -152,12 +157,12 @@
       var options = Options.init()
       var verbose = false
 
-
       val getopts = Getopts("""
 Usage: isabelle process_theories [OPTIONS] [THEORIES...]
 
   Options are:
     -D DIR       explicit session directory (default: private)
+    -E EXPORTS   write session export artifacts to file-system
     -F FILE      include additional session files, listed in FILE
     -H REGEX     filter messages by matching against head
     -M REGEX     filter messages by matching against body
@@ -173,6 +178,7 @@
   Process theories within an adhoc session context.
 """,
         "D:" -> (arg => directory = Some(Path.explode(arg))),
+        "E:" -> (arg => export_files += Sessions.parse_exports(arg)),
         "F:" -> (arg => files ++= read_files(Path.explode(arg))),
         "H:" -> (arg => message_head += arg.r),
         "M:" -> (arg => message_body += arg.r),
@@ -194,7 +200,7 @@
           process_theories(options, logic, directory = directory, theories = theories,
             files = files.toList, dirs = dirs.toList, output_messages = output_messages,
             message_head = message_head.toList, message_body = message_body.toList,
-            margin = margin, unicode_symbols = unicode_symbols,
+            margin = margin, unicode_symbols = unicode_symbols, export_files = export_files.toList,
             progress = progress)
         }