Process theories within an adhoc session context.
--- a/etc/build.props Sun Aug 10 12:27:39 2025 +0200
+++ b/etc/build.props Sun Aug 10 15:17:13 2025 +0200
@@ -235,6 +235,7 @@
src/Pure/Tools/phabricator.scala \
src/Pure/Tools/print_operation.scala \
src/Pure/Tools/prismjs.scala \
+ src/Pure/Tools/process_theories.scala \
src/Pure/Tools/profiling.scala \
src/Pure/Tools/profiling_report.scala \
src/Pure/Tools/scala_build.scala \
--- a/src/Pure/Build/build.scala Sun Aug 10 12:27:39 2025 +0200
+++ b/src/Pure/Build/build.scala Sun Aug 10 15:17:13 2025 +0200
@@ -126,11 +126,16 @@
}
final def build_store(options: Options,
+ private_dir: Option[Path] = None,
build_cluster: Boolean = false,
cache: Rich_Text.Cache = Rich_Text.Cache.make()
): Store = {
val build_options = engine.build_options(options, build_cluster = build_cluster)
- val store = Store(build_options, build_cluster = build_cluster, cache = cache)
+ val store =
+ Store(build_options,
+ private_dir = private_dir,
+ build_cluster = build_cluster,
+ cache = cache)
Isabelle_System.make_directory(store.output_dir + Path.basic("log"))
Isabelle_Fonts.init()
store
@@ -162,6 +167,7 @@
def build(
options: Options,
+ private_dir: Option[Path] = None,
build_hosts: List[Build_Cluster.Host] = Nil,
selection: Sessions.Selection = Sessions.Selection.empty,
browser_info: Browser_Info.Config = Browser_Info.Config.none,
@@ -185,7 +191,11 @@
cache: Rich_Text.Cache = Rich_Text.Cache.make()
): Results = {
val engine = Engine(engine_name(options))
- val store = engine.build_store(options, build_cluster = build_hosts.nonEmpty, cache = cache)
+ val store =
+ engine.build_store(options,
+ private_dir = private_dir,
+ build_cluster = build_hosts.nonEmpty,
+ cache = cache)
val build_options = store.options
using(store.open_server()) { server =>
@@ -294,6 +304,7 @@
/* build logic image */
def build_logic(options: Options, logic: String,
+ private_dir: Option[Path] = None,
progress: Progress = new Progress,
build_heap: Boolean = false,
dirs: List[Path] = Nil,
--- a/src/Pure/Build/sessions.scala Sun Aug 10 12:27:39 2025 +0200
+++ b/src/Pure/Build/sessions.scala Sun Aug 10 15:17:13 2025 +0200
@@ -619,11 +619,14 @@
chapter_defs: Chapter_Defs = Chapter_Defs.empty,
chapter: String = UNSORTED,
dir_selected: Boolean = false,
+ draft_session: Boolean = false
): Info = {
try {
- val name = entry.name
+ val name =
+ if (draft_session) DRAFT
+ else if (illegal_session(entry.name)) error("Illegal session name " + quote(entry.name))
+ else entry.name
- if (illegal_session(name)) error("Illegal session name " + quote(name))
if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
--- a/src/Pure/System/isabelle_tool.scala Sun Aug 10 12:27:39 2025 +0200
+++ b/src/Pure/System/isabelle_tool.scala Sun Aug 10 15:17:13 2025 +0200
@@ -150,6 +150,7 @@
Phabricator.isabelle_tool2,
Phabricator.isabelle_tool3,
Phabricator.isabelle_tool4,
+ Process_Theories.isabelle_tool,
Profiling.isabelle_tool,
Profiling_Report.isabelle_tool,
Scala_Project.isabelle_tool,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/process_theories.scala Sun Aug 10 15:17:13 2025 +0200
@@ -0,0 +1,141 @@
+/* Title: Pure/Tools/process_theories.scala
+ Author: Makarius
+
+Process theories within an adhoc session context.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+import scala.collection.mutable
+
+
+object Process_Theories {
+ /** process theories **/
+
+ def read_files(path: Path): List[Path] =
+ Library.trim_split_lines(File.read(path)).map(Path.explode)
+
+ def process_theories(
+ options: Options,
+ logic: String,
+ theories: List[String],
+ files: List[Path] = Nil,
+ dirs: List[Path] = Nil,
+ progress: Progress = new Progress
+ ): Build.Results = {
+ Isabelle_System.with_tmp_dir("private") { private_dir =>
+ /* options */
+
+ val build_engine = Build.Engine(Build.engine_name(options))
+ val build_options = build_engine.build_options(options)
+
+
+ /* session directory and files */
+
+ val session_dir = Isabelle_System.make_directory(private_dir + Path.basic("session"))
+
+ {
+ 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)
+ }
+ Isabelle_System.copy_file(path, target)
+ }
+ }
+ }
+
+ /* session theories */
+
+ val more_theories =
+ for (path <- files; name <- Thy_Header.get_thy_name(path.implode))
+ yield name
+
+ val session_theories = theories ::: more_theories
+
+
+ /* session imports */
+
+ val sessions_structure = Sessions.load_structure(build_options, dirs = dirs)
+
+ val session_imports =
+ Set.from(
+ for {
+ name <- session_theories.iterator
+ session = sessions_structure.theory_qualifier(name)
+ if session.nonEmpty
+ } yield session).toList
+
+
+ /* build adhoc session */
+
+ val session_entry =
+ Sessions.Session_Entry(
+ parent = Some(logic),
+ theories = session_theories.map(a => (Nil, List(((a, Position.none), false)))),
+ imports = session_imports)
+
+ val session_info =
+ Sessions.Info.make(session_entry, draft_session = true,
+ dir = session_dir, options = options)
+
+ Build.build(options, private_dir = Some(private_dir), progress = progress,
+ infos = List(session_info), selection = Sessions.Selection.session(session_info.name))
+ }
+ }
+
+
+
+ /** Isabelle tool wrapper **/
+
+ val isabelle_tool = Isabelle_Tool("process_theories",
+ "process theories within an adhoc session context",
+ Scala_Project.here,
+ { args =>
+ val dirs = new mutable.ListBuffer[Path]
+ val files = new mutable.ListBuffer[Path]
+ var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+ var options = Options.init()
+ var verbose = false
+
+ val getopts = Getopts("""
+Usage: isabelle process_theories [OPTIONS] [THEORIES...]
+
+ Options are:
+ -F FILE include addition session files, listed in FILE
+ -d DIR include session directory
+ -f FILE include addition session files
+ -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -v verbose
+
+ Process theories within an adhoc session context.
+""",
+ "F:" -> (arg => files ++= read_files(Path.explode(arg))),
+ "d:" -> (arg => dirs += Path.explode(arg)),
+ "f:" -> (arg => files += Path.explode(arg)),
+ "l:" -> (arg => logic = arg),
+ "o:" -> (arg => options = options + arg),
+ "v" -> (_ => verbose = true))
+
+ val theories = getopts(args)
+
+ val progress = new Console_Progress(verbose = verbose)
+
+ val results =
+ progress.interrupt_handler {
+ process_theories(options, logic, theories, files = files.toList, dirs = dirs.toList,
+ progress = progress)
+ }
+
+ sys.exit(results.rc)
+ })
+}