--- a/NEWS Sun Aug 10 23:30:55 2025 +0200
+++ b/NEWS Sun Aug 10 23:32:06 2025 +0200
@@ -335,6 +335,19 @@
*** System ***
+* The command-line tool "isabelle process_theories" tool takes source
+files and theories within a proper session context (like regular
+"isabelle build"). Output of prover messages works roughly like
+"isabelle build_log", while the theories are being processed.
+
+Examples:
+
+ isabelle process_theories -O HOL-Library.Multiset
+
+ isabelle process_theories -O -o show_states HOL-Library.Multiset
+
+ isabelle process_theories -f '~~/src/HOL/Examples/Seq.thy'
+
* System option "show_results" (default true) controls output of
toplevel command results (definitions, theorems) in batch-builds. In
interactive mode this is always enabled; in batch-builds it can be
--- a/src/Doc/System/Environment.thy Sun Aug 10 23:30:55 2025 +0200
+++ b/src/Doc/System/Environment.thy Sun Aug 10 23:32:06 2025 +0200
@@ -303,6 +303,15 @@
section \<open>The raw Isabelle ML process\<close>
+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.
+\<close>
+
+
subsection \<open>Batch mode \label{sec:tool-process}\<close>
text \<open>
--- a/src/Doc/System/Sessions.thy Sun Aug 10 23:30:55 2025 +0200
+++ b/src/Doc/System/Sessions.thy Sun Aug 10 23:32:06 2025 +0200
@@ -1196,4 +1196,81 @@
@{verbatim [display] \<open> isabelle build_task -A: -X slow -g AFP\<close>}
\<close>
+
+section \<open>Process theories within a session context \label{sec:tool-process-theories}\<close>
+
+text \<open>
+ The @{tool_def process_theories} tool takes source files and theories from
+ existing sessions to compose an adhoc session (in a temporary directory)
+ that is then processed via regular @{tool build}. It is also possible to
+ output prover messages roughly like @{tool build_log}, while the theories
+ are being processed.
+
+ @{verbatim [display]
+\<open>Usage: isabelle process_theories [OPTIONS] [THEORIES...]
+
+ Options are:
+ -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
+ -O output messages
+ -d DIR include session directory
+ -f FILE include addition session files
+ -l NAME logic session name (default ISABELLE_LOGIC="HOL")
+ -m MARGIN margin for pretty printing (default: 76.0)
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -v verbose
+
+ 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>
+ or \<^verbatim>\<open>HOL-Examples.Seq\<close>. The session qualifiers are used to augment the adhoc
+ session specification by suitable entries for \isakeyword{sessions}
+ (\secref{sec:session-root}).
+
+ \<^medskip>
+ Options \<^verbatim>\<open>-f\<close> and \<^verbatim>\<open>-F\<close> specify source files for the adhoc session directory
+ (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.
+
+ \<^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}.
+
+ Option \<^verbatim>\<open>-O\<close> enables output of prover messages. Options \<^verbatim>\<open>-H\<close>, \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-m\<close>
+ work as in @{tool build_log}.
+\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+ Process a theory from a different session in the context of the default
+ logic (\<^verbatim>\<open>HOL\<close>):
+
+ @{verbatim [display] \<open> isabelle process_theories HOL-Library.Multiset\<close>}
+
+ \<^smallskip>
+ Process a theory with prover output enabled:
+ @{verbatim [display] \<open> isabelle process_theories -O HOL-Library.Multiset\<close>}
+
+ \<^smallskip>
+ Process a theory with prover output enabled, including proof states:
+ @{verbatim [display] \<open> isabelle process_theories -O -o show_states HOL-Library.Multiset\<close>}
+
+ \<^smallskip>
+ Process a self-contained theory file from the Isabelle distribution, outside
+ of its original session context:
+ @{verbatim [display] \<open> isabelle process_theories -f '~~/src/HOL/Examples/Seq.thy'\<close>}
+
+\<close>
+
end