# HG changeset patch # User wenzelm # Date 1754831833 -7200 # Node ID a28d9192d31eb7fe72da3041003c10f833192d7d # Parent 9c34a176817897477bd3fac837408beb534b7208 Process theories within an adhoc session context. diff -r 9c34a1768178 -r a28d9192d31e etc/build.props --- 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 \ diff -r 9c34a1768178 -r a28d9192d31e src/Pure/Build/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, diff -r 9c34a1768178 -r a28d9192d31e src/Pure/Build/sessions.scala --- 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") diff -r 9c34a1768178 -r a28d9192d31e src/Pure/System/isabelle_tool.scala --- 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, diff -r 9c34a1768178 -r a28d9192d31e src/Pure/Tools/process_theories.scala --- /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) + }) +}