--- a/src/Pure/ML/ml_process.scala Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Pure/ML/ml_process.scala Fri Dec 16 18:12:48 2022 +0100
@@ -13,7 +13,7 @@
object ML_Process {
def apply(options: Options,
- background: Sessions.Background,
+ session_background: Sessions.Background,
store: Sessions.Store,
logic: String = "",
raw_ml_system: Boolean = false,
@@ -31,7 +31,7 @@
val heaps: List[String] =
if (raw_ml_system) Nil
else {
- background.sessions_structure.selection(logic_name).
+ session_background.sessions_structure.selection(logic_name).
build_requirements(List(logic_name)).
map(a => File.platform_path(store.the_heap(a)))
}
@@ -80,8 +80,7 @@
val eval_init_session = if (raw_ml_system) Nil else List("Resources.init_session_env ()")
val init_session = Isabelle_System.tmp_file("init_session")
Isabelle_System.chmod("600", File.path(init_session))
- val resources = new Resources(background.sessions_structure, background.base)
- File.write(init_session, resources.init_session_yxml)
+ File.write(init_session, new Resources(session_background).init_session_yxml)
// process
val eval_process =
@@ -169,11 +168,11 @@
val more_args = getopts(args)
if (args.isEmpty || more_args.nonEmpty) getopts.usage()
- val background = Sessions.background(options, logic, dirs = dirs).check_errors
+ val session_background = Sessions.background(options, logic, dirs = dirs).check_errors
val store = Sessions.store(options)
val result =
- ML_Process(options, background, store, logic = logic, args = eval_args, modes = modes)
- .result(
+ ML_Process(options, session_background, store,
+ logic = logic, args = eval_args, modes = modes).result(
progress_stdout = Output.writeln(_, stdout = true),
progress_stderr = Output.writeln(_))
--- a/src/Pure/PIDE/headless.scala Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Pure/PIDE/headless.scala Fri Dec 16 18:12:48 2022 +0100
@@ -445,9 +445,9 @@
object Resources {
def apply(
options: Options,
- background: Sessions.Background,
+ session_background: Sessions.Background,
log: Logger = No_Logger
- ): Resources = new Resources(options, background, log = log)
+ ): Resources = new Resources(options, session_background, log = log)
def make(
options: Options,
@@ -457,10 +457,10 @@
progress: Progress = new Progress,
log: Logger = No_Logger
): Resources = {
- val background =
+ val session_background =
Sessions.background(options, session_name, dirs = session_dirs,
include_sessions = include_sessions, progress = progress)
- apply(options, background, log = log)
+ apply(options, session_background, log = log)
}
final class Theory private[Headless](
@@ -603,15 +603,13 @@
class Resources private[Headless](
val options: Options,
- val session_background: Sessions.Background,
+ session_background: Sessions.Background,
log: Logger = No_Logger)
- extends isabelle.Resources(
- session_background.sessions_structure,
- session_background.check_errors.base,
- log = log
- ) {
+ extends isabelle.Resources(session_background, log = log) {
resources =>
+ session_background.check_errors
+
val store: Sessions.Store = Sessions.store(options)
--- a/src/Pure/PIDE/resources.scala Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Pure/PIDE/resources.scala Fri Dec 16 18:12:48 2022 +0100
@@ -13,7 +13,7 @@
object Resources {
- def bootstrap: Resources = new Resources(Sessions.Structure.empty, Sessions.Base.bootstrap)
+ def bootstrap: Resources = new Resources(Sessions.Background(base = Sessions.Base.bootstrap))
def hidden_node(name: Document.Node.Name): Boolean =
!name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
@@ -23,13 +23,15 @@
}
class Resources(
- val sessions_structure: Sessions.Structure,
- val session_base: Sessions.Base,
+ val session_background: Sessions.Background,
val log: Logger = No_Logger,
command_timings: List[Properties.T] = Nil
) {
resources =>
+ def sessions_structure: Sessions.Structure = session_background.sessions_structure
+ def session_base: Sessions.Base = session_background.base
+ def session_errors: List[String] = session_background.errors
override def toString: String = "Resources(" + session_base.toString + ")"
--- a/src/Pure/Thy/sessions.scala Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Dec 16 18:12:48 2022 +0100
@@ -266,7 +266,9 @@
val info = sessions_structure(session_name)
try {
val deps_base = info.deps_base(session_bases)
- val resources = new Resources(sessions_structure, deps_base)
+ val session_background =
+ Sessions.Background(base = deps_base, sessions_structure = sessions_structure)
+ val resources = new Resources(session_background)
if (verbose || list_files) {
val groups =
--- a/src/Pure/Tools/build_job.scala Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Pure/Tools/build_job.scala Fri Dec 16 18:12:48 2022 +0100
@@ -274,8 +274,7 @@
else Nil
val resources =
- new Resources(session_background.sessions_structure, session_background.base, log = log,
- command_timings = command_timings0)
+ new Resources(session_background, log = log, command_timings = command_timings0)
val session =
new Session(options, resources) {
override val cache: Term.Cache = store.cache
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Dec 16 18:12:48 2022 +0100
@@ -71,11 +71,7 @@
val options: Options,
session_background: Sessions.Background,
log: Logger = No_Logger)
-extends Resources(
- session_background.sessions_structure,
- session_background.check_errors.base,
- log = log
-) {
+extends Resources(session_background, log = log) {
resources =>
private val state = Synchronized(VSCode_Resources.State())
--- a/src/Tools/jEdit/src/jedit_resources.scala Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Fri Dec 16 18:12:48 2022 +0100
@@ -26,11 +26,8 @@
new JEdit_Resources(JEdit_Sessions.session_background(options))
}
-class JEdit_Resources private(val session_background: Sessions.Background)
-extends Resources(session_background.sessions_structure, session_background.base) {
- def session_errors: List[String] = session_background.errors
-
-
+class JEdit_Resources private(session_background: Sessions.Background)
+extends Resources(session_background) {
/* document node name */
def node_name(path: String): Document.Node.Name =