# HG changeset patch
# User wenzelm
# Date 1754910996 -7200
# Node ID 96010245b7315a29e0ad8f5ad6f22720f0f22f77
# Parent  50673a1d90f295027e737ba42cc10487a819d55c
support for explicit session directory;

diff -r 50673a1d90f2 -r 96010245b731 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Aug 11 13:00:50 2025 +0200
+++ b/src/Doc/System/Sessions.thy	Mon Aug 11 13:16:36 2025 +0200
@@ -1210,6 +1210,7 @@
 \<open>Usage: isabelle process_theories [OPTIONS] [THEORIES...]
 
   Options are:
+    -D DIR       explicit session directory (default: private)
     -F FILE      include addition session files, listed in FILE
     -H REGEX     filter messages by matching against head
     -M REGEX     filter messages by matching against body
@@ -1222,8 +1223,7 @@
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose
 
-  Process theories within an adhoc session context.
-\<close>}
+  Process theories within an adhoc session context.\<close>}
 
   Explicit \<^emph>\<open>theories\<close> given as command-line arguments, not options, refer to
   qualified theory names from existing sessions, e.g. \<^verbatim>\<open>HOL-Library.Multiset\<close>
@@ -1236,10 +1236,14 @@
   (multiple occurrences are possible): \<^verbatim>\<open>-f\<close> is for literal file names, and
   \<^verbatim>\<open>-F\<close> is for files that contain a list of further files (one per line).
 
-  All source files are copied to the private (temporary) session directory,
-  without any subdirectory structure. Files with extension \<^verbatim>\<open>.thy\<close> are treated
-  as theory files: their base names are appended to the overall list of
-  \<^emph>\<open>theories\<close>, and thus loaded into the adhoc session, too.
+  Option \<^verbatim>\<open>-D\<close> indicates an explicit session directory, instead of a private
+  temporary one. This directory must not be used by another session already.
+
+  If option \<^verbatim>\<open>-D\<close> is \<^emph>\<open>not\<close> given, then all source files are copied to the
+  adhoc session directory, without any subdirectory structure. Files with
+  extension \<^verbatim>\<open>.thy\<close> are treated as theory files: their base names are appended
+  to the overall list of \<^emph>\<open>theories\<close>, and thus loaded into the adhoc session,
+  too.
 
   \<^medskip>
   Option \<^verbatim>\<open>-l\<close> specifies the parent logic session, which is produced on the
diff -r 50673a1d90f2 -r 96010245b731 src/Pure/Tools/process_theories.scala
--- a/src/Pure/Tools/process_theories.scala	Mon Aug 11 13:00:50 2025 +0200
+++ b/src/Pure/Tools/process_theories.scala	Mon Aug 11 13:16:36 2025 +0200
@@ -22,6 +22,7 @@
   def process_theories(
     options: Options,
     logic: String,
+    directory: Option[Path] = None,
     theories: List[String] = Nil,
     files: List[Path] = Nil,
     dirs: List[Path] = Nil,
@@ -46,23 +47,26 @@
       val private_prefix = private_dir.implode + "/"
 
       val session_name = Sessions.DRAFT
-      val session_dir = Isabelle_System.make_directory(private_dir + Path.basic(session_name))
-
-      {
-        var seen = Set.empty[JFile]
-        for (path0 <- files) {
-          val path = path0.canonical
-          val file = path.file
-          if (!seen(file)) {
-            seen += file
-            val target = session_dir + path.base
-            if (target.is_file) {
-              error("Duplicate session source file " + path.base + " --- from " + path)
+      val session_dir =
+        directory match {
+          case Some(dir) => dir.absolute
+          case None =>
+            val dir = Isabelle_System.make_directory(private_dir + Path.basic(session_name))
+            var seen = Set.empty[JFile]
+            for (path0 <- files) {
+              val path = path0.canonical
+              val file = path.file
+              if (!seen(file)) {
+                seen += file
+                val target = dir + path.base
+                if (target.is_file) {
+                  error("Duplicate session source file " + path.base + " --- from " + path)
+                }
+                Isabelle_System.copy_file(path, target)
+              }
             }
-            Isabelle_System.copy_file(path, target)
-          }
+            dir
         }
-      }
 
       /* session theories */
 
@@ -133,6 +137,7 @@
     "process theories within an adhoc session context",
     Scala_Project.here,
     { args =>
+      var directory: Option[Path] = None
       val message_head = new mutable.ListBuffer[Regex]
       val message_body = new mutable.ListBuffer[Regex]
       var output_messages = false
@@ -149,6 +154,7 @@
 Usage: isabelle process_theories [OPTIONS] [THEORIES...]
 
   Options are:
+    -D DIR       explicit session directory (default: private)
     -F FILE      include addition session files, listed in FILE
     -H REGEX     filter messages by matching against head
     -M REGEX     filter messages by matching against body
@@ -163,6 +169,7 @@
 
   Process theories within an adhoc session context.
 """,
+        "D:" -> (arg => directory = Some(Path.explode(arg))),
         "F:" -> (arg => files ++= read_files(Path.explode(arg))),
         "H:" -> (arg => message_head += arg.r),
         "M:" -> (arg => message_body += arg.r),
@@ -181,9 +188,10 @@
 
       val results =
         progress.interrupt_handler {
-          process_theories(options, logic, 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,
+          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,
             progress = progress)
         }