--- a/src/Pure/Admin/build_doc.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/Admin/build_doc.scala Fri Dec 16 20:14:41 2022 +0100
@@ -54,7 +54,7 @@
progress.expose_interrupt()
progress.echo("Documentation " + quote(doc) + " ...")
- using(Export.open_session_context(build_results.store, deps.base_info(session))) {
+ using(Export.open_session_context(build_results.store, deps.background(session))) {
session_context =>
Document_Build.build_documents(
Document_Build.context(session_context),
--- a/src/Pure/ML/ml_console.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/ML/ml_console.scala Fri Dec 16 20:14:41 2022 +0100
@@ -48,7 +48,6 @@
if (more_args.nonEmpty) getopts.usage()
- val sessions_structure = Sessions.load_structure(options, dirs = dirs)
val store = Sessions.store(options)
// build logic
@@ -61,16 +60,23 @@
if (rc != Process_Result.RC.ok) sys.exit(rc)
}
+ val background =
+ if (raw_ml_system) {
+ Sessions.Background(
+ base = Sessions.Base.bootstrap,
+ sessions_structure = Sessions.load_structure(options, dirs = dirs))
+ }
+ else {
+ Sessions.background(
+ options, logic, dirs = dirs, include_sessions = include_sessions).check_errors
+ }
+
// process loop
val process =
- ML_Process(options, sessions_structure, store,
+ ML_Process(options, background, store,
logic = logic, args = List("-i"), redirect = true,
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
- raw_ml_system = raw_ml_system,
- session_base =
- if (raw_ml_system) None
- else Some(Sessions.base_info(
- options, logic, dirs = dirs, include_sessions = include_sessions).check_errors.base))
+ raw_ml_system = raw_ml_system)
POSIX_Interrupt.handler { process.interrupt() } {
new TTY_Loop(process.stdin, process.stdout).join()
--- a/src/Pure/ML/ml_process.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/ML/ml_process.scala Fri Dec 16 20:14:41 2022 +0100
@@ -13,7 +13,7 @@
object ML_Process {
def apply(options: Options,
- sessions_structure: Sessions.Structure,
+ session_background: Sessions.Background,
store: Sessions.Store,
logic: String = "",
raw_ml_system: Boolean = false,
@@ -24,15 +24,14 @@
cwd: JFile = null,
env: JMap[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
- cleanup: () => Unit = () => (),
- session_base: Option[Sessions.Base] = None
+ cleanup: () => Unit = () => ()
): Bash.Process = {
val logic_name = Isabelle_System.default_logic(logic)
val heaps: List[String] =
if (raw_ml_system) Nil
else {
- 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)))
}
@@ -77,15 +76,11 @@
Isabelle_System.chmod("600", File.path(isabelle_process_options))
File.write(isabelle_process_options, YXML.string_of_body(options.encode))
- // session base
- val (init_session_base, eval_init_session) =
- session_base match {
- case None => (Sessions.bootstrap_base, Nil)
- case Some(base) => (base, List("Resources.init_session_env ()"))
- }
+ // session resources
+ 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))
- File.write(init_session, new Resources(sessions_structure, init_session_base).init_session_yxml)
+ File.write(init_session, new Resources(session_background).init_session_yxml)
// process
val eval_process =
@@ -173,11 +168,11 @@
val more_args = getopts(args)
if (args.isEmpty || more_args.nonEmpty) getopts.usage()
- val base_info = Sessions.base_info(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, base_info.sessions_structure, store, logic = logic, args = eval_args,
- modes = modes, session_base = Some(base_info.base)).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/document_info.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/PIDE/document_info.scala Fri Dec 16 20:14:41 2022 +0100
@@ -113,7 +113,7 @@
def read_session(session_name: String): Document_Info.Session = {
val static_theories = deps(session_name).used_theories.map(_._1.theory)
val (thys, build_uuid) = {
- using(database_context.open_session(deps.base_info(session_name))) { session_context =>
+ using(database_context.open_session(deps.background(session_name))) { session_context =>
val thys =
for {
theory_name <- static_theories
--- a/src/Pure/PIDE/headless.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/PIDE/headless.scala Fri Dec 16 20:14:41 2022 +0100
@@ -443,8 +443,11 @@
/** resources **/
object Resources {
- def apply(options: Options, base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources =
- new Resources(options, base_info, log = log)
+ def apply(
+ options: Options,
+ session_background: Sessions.Background,
+ log: Logger = No_Logger
+ ): Resources = new Resources(options, session_background, log = log)
def make(
options: Options,
@@ -454,10 +457,10 @@
progress: Progress = new Progress,
log: Logger = No_Logger
): Resources = {
- val base_info =
- Sessions.base_info(options, session_name, dirs = session_dirs,
+ val session_background =
+ Sessions.background(options, session_name, dirs = session_dirs,
include_sessions = include_sessions, progress = progress)
- apply(options, base_info, log = log)
+ apply(options, session_background, log = log)
}
final class Theory private[Headless](
@@ -600,15 +603,13 @@
class Resources private[Headless](
val options: Options,
- val session_base_info: Sessions.Base_Info,
+ session_background: Sessions.Background,
log: Logger = No_Logger)
- extends isabelle.Resources(
- session_base_info.sessions_structure,
- session_base_info.check_errors.base,
- log = log
- ) {
+ extends isabelle.Resources(session_background, log = log) {
resources =>
+ session_background.check_errors
+
val store: Sessions.Store = Sessions.store(options)
@@ -618,11 +619,11 @@
print_mode: List[String] = Nil,
progress: Progress = new Progress
): Session = {
- val session_name = session_base_info.session_name
+ val session_name = session_background.session_name
val session = new Session(session_name, options, resources)
progress.echo("Starting session " + session_name + " ...")
- Isabelle_Process.start(session, options, session_base_info.sessions_structure, store,
+ Isabelle_Process.start(session, options, session_background, store,
logic = session_name, modes = print_mode).await_startup()
session
--- a/src/Pure/PIDE/resources.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/PIDE/resources.scala Fri Dec 16 20:14:41 2022 +0100
@@ -13,8 +13,7 @@
object Resources {
- def empty: Resources =
- new Resources(Sessions.Structure.empty, Sessions.Structure.empty.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)
@@ -24,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/System/isabelle_process.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/System/isabelle_process.scala Fri Dec 16 20:14:41 2022 +0100
@@ -15,7 +15,7 @@
def start(
session: Session,
options: Options,
- sessions_structure: Sessions.Structure,
+ session_background: Sessions.Background,
store: Sessions.Store,
logic: String = "",
raw_ml_system: Boolean = false,
@@ -31,7 +31,7 @@
val channel_options =
options.string.update("system_channel_address", channel.address).
string.update("system_channel_password", channel.password)
- ML_Process(channel_options, sessions_structure, store,
+ ML_Process(channel_options, session_background, store,
logic = logic, raw_ml_system = raw_ml_system,
use_prelude = use_prelude, eval_main = eval_main,
modes = modes, cwd = cwd, env = env)
--- a/src/Pure/Thy/browser_info.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/Thy/browser_info.scala Fri Dec 16 20:14:41 2022 +0100
@@ -694,7 +694,7 @@
context1.update_root()
Par_List.map({ (session: String) =>
- using(database_context.open_session(deps.base_info(session))) { session_context =>
+ using(database_context.open_session(deps.background(session))) { session_context =>
build_session(context1, session_context, progress = progress, verbose = verbose)
}
}, sessions1)
--- a/src/Pure/Thy/document_build.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/Thy/document_build.scala Fri Dec 16 20:14:41 2022 +0100
@@ -511,13 +511,13 @@
Sessions.load_structure(options + "document=pdf", dirs = dirs).
selection_deps(Sessions.Selection.session(session))
- val session_base_info = deps.base_info(session)
+ val session_background = deps.background(session)
if (output_sources.isEmpty && output_pdf.isEmpty) {
progress.echo_warning("No output directory")
}
- using(Export.open_session_context(build_results.store, session_base_info)) {
+ using(Export.open_session_context(build_results.store, session_background)) {
session_context =>
build_documents(
context(session_context, progress = progress),
--- a/src/Pure/Thy/export.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/Thy/export.scala Fri Dec 16 20:14:41 2022 +0100
@@ -251,11 +251,11 @@
def open_session_context(
store: Sessions.Store,
- session_base_info: Sessions.Base_Info,
+ session_background: Sessions.Background,
document_snapshot: Option[Document.Snapshot] = None
): Session_Context = {
open_database_context(store).open_session(
- session_base_info, document_snapshot = document_snapshot, close_database_context = true)
+ session_background, document_snapshot = document_snapshot, close_database_context = true)
}
class Database_Context private[Export](
@@ -287,15 +287,15 @@
}
def open_session0(session: String, close_database_context: Boolean = false): Session_Context =
- open_session(Sessions.base_info0(session), close_database_context = close_database_context)
+ open_session(Sessions.background0(session), close_database_context = close_database_context)
def open_session(
- session_base_info: Sessions.Base_Info,
+ session_background: Sessions.Background,
document_snapshot: Option[Document.Snapshot] = None,
close_database_context: Boolean = false
): Session_Context = {
- val session_name = session_base_info.check_errors.session_name
- val session_hierarchy = session_base_info.sessions_structure.build_hierarchy(session_name)
+ val session_name = session_background.check_errors.session_name
+ val session_hierarchy = session_background.sessions_structure.build_hierarchy(session_name)
val session_databases =
database_server match {
case Some(db) => session_hierarchy.map(name => new Session_Database(name, db))
@@ -312,7 +312,8 @@
}
}
}
- new Session_Context(database_context, session_base_info, session_databases, document_snapshot) {
+ new Session_Context(
+ database_context, session_background, session_databases, document_snapshot) {
override def close(): Unit = {
session_databases.foreach(_.close())
if (close_database_context) database_context.close()
@@ -331,7 +332,7 @@
class Session_Context private[Export](
val database_context: Database_Context,
- session_base_info: Sessions.Base_Info,
+ session_background: Sessions.Background,
db_hierarchy: List[Session_Database],
document_snapshot: Option[Document.Snapshot]
) extends AutoCloseable {
@@ -341,9 +342,9 @@
def cache: Term.Cache = database_context.cache
- def sessions_structure: Sessions.Structure = session_base_info.sessions_structure
+ def sessions_structure: Sessions.Structure = session_background.sessions_structure
- def session_base: Sessions.Base = session_base_info.base
+ def session_base: Sessions.Base = session_background.base
def session_name: String =
if (document_snapshot.isDefined) Sessions.DRAFT
--- a/src/Pure/Thy/sessions.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Dec 16 20:14:41 2022 +0100
@@ -56,6 +56,10 @@
/* base info */
+ object Base {
+ val bootstrap: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax)
+ }
+
sealed case class Base(
session_name: String = "",
session_pos: Position.T = Position.none,
@@ -97,9 +101,7 @@
nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
}
- val bootstrap_base: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax)
-
- sealed case class Base_Info(
+ sealed case class Background(
base: Base,
sessions_structure: Structure = Structure.empty,
errors: List[String] = Nil,
@@ -107,22 +109,22 @@
) {
def session_name: String = base.session_name
- def check_errors: Base_Info =
+ def check_errors: Background =
if (errors.isEmpty) this
else error(cat_lines(errors))
}
- def base_info0(session: String): Base_Info =
- Base_Info(Base(session_name = session))
+ def background0(session: String): Background =
+ Background(Base(session_name = session))
- def base_info(options: Options,
+ def background(options: Options,
session: String,
progress: Progress = new Progress,
dirs: List[Path] = Nil,
include_sessions: List[String] = Nil,
session_ancestor: Option[String] = None,
session_requirements: Boolean = false
- ): Base_Info = {
+ ): Background = {
val full_sessions = load_structure(options, dirs = dirs)
val selected_sessions =
@@ -192,7 +194,7 @@
val deps1 = Sessions.deps(selected_sessions1, progress = progress)
- Base_Info(deps1(session1), sessions_structure = full_sessions1,
+ Background(deps1(session1), sessions_structure = full_sessions1,
errors = deps1.errors, infos = infos1)
}
@@ -200,8 +202,8 @@
/* source dependencies */
sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) {
- def base_info(session: String): Base_Info =
- Base_Info(base = apply(session), sessions_structure = sessions_structure, errors = errors)
+ def background(session: String): Background =
+ Background(base = apply(session), sessions_structure = sessions_structure, errors = errors)
def is_empty: Boolean = session_bases.keysIterator.forall(_.isEmpty)
def apply(name: String): Base = session_bases(name)
@@ -257,14 +259,16 @@
val session_bases =
sessions_structure.imports_topological_order.foldLeft(
- Map(Sessions.bootstrap_base.session_entry)) {
+ Map(Sessions.Base.bootstrap.session_entry)) {
case (session_bases, session_name) =>
progress.expose_interrupt()
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 =
@@ -792,8 +796,6 @@
) {
sessions_structure =>
- def bootstrap: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax)
-
def dest_session_directories: List[(String, String)] =
for ((file, session) <- session_directories.toList)
yield (File.standard_path(file), session)
--- a/src/Pure/Tools/build_job.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/Tools/build_job.scala Fri Dec 16 20:14:41 2022 +0100
@@ -99,7 +99,7 @@
unicode_symbols: Boolean = false
): Unit = {
val store = Sessions.store(options)
- val session = new Session(options, Resources.empty)
+ val session = new Session(options, Resources.bootstrap)
def check(filter: List[Regex], make_string: => String): Boolean =
filter.isEmpty || {
@@ -249,7 +249,7 @@
) {
val options: Options = NUMA.policy_options(info.options, numa_node)
- private val sessions_structure = deps.sessions_structure
+ private val session_background = deps.background(session_name)
private val future_result: Future[Process_Result] =
Future.thread("build", uninterruptible = true) {
@@ -274,7 +274,7 @@
else Nil
val resources =
- new Resources(sessions_structure, 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
@@ -450,7 +450,7 @@
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
val process =
- Isabelle_Process.start(session, options, sessions_structure, store,
+ Isabelle_Process.start(session, options, session_background, store,
logic = parent, raw_ml_system = is_pure,
use_prelude = use_prelude, eval_main = eval_main,
cwd = info.dir.file, env = env)
@@ -488,7 +488,7 @@
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
using(Export.open_database_context(store)) { database_context =>
val documents =
- using(database_context.open_session(deps.base_info(session_name))) {
+ using(database_context.open_session(deps.background(session_name))) {
session_context =>
Document_Build.build_documents(
Document_Build.context(session_context, progress = progress),
--- a/src/Pure/Tools/jedit.ML Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/Tools/jedit.ML Fri Dec 16 20:14:41 2022 +0100
@@ -40,7 +40,7 @@
(parse_resources o map File.read)
[\<^file>\<open>~~/src/Tools/jEdit/jedit_main/actions.xml\<close>,
\<^file>\<open>~~/src/Tools/jEdit/jedit_main/dockables.xml\<close>] @
- (parse_resources o \<^scala>\<open>jEdit.resources\<close>) ["actions.xml", "dockables.xml"]
+ (parse_resources o \<^scala>\<open>jEdit.resource\<close>) ["actions.xml", "dockables.xml"]
|> sort_strings);
fun get_actions () = Lazy.force lazy_actions;
--- a/src/Pure/Tools/server_commands.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Pure/Tools/server_commands.scala Fri Dec 16 20:14:41 2022 +0100
@@ -62,12 +62,12 @@
def command(
args: Args,
progress: Progress = new Progress
- ) : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) = {
+ ) : (JSON.Object.T, Build.Results, Options, Sessions.Background) = {
val options = Options.init(prefs = args.preferences, opts = args.options)
val dirs = args.dirs.map(Path.explode)
- val base_info =
- Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
+ val session_background =
+ Sessions.background(options, args.session, progress = progress, dirs = dirs,
include_sessions = args.include_sessions).check_errors
val results =
@@ -76,11 +76,11 @@
progress = progress,
build_heap = true,
dirs = dirs,
- infos = base_info.infos,
+ infos = session_background.infos,
verbose = args.verbose)
val sessions_order =
- base_info.sessions_structure.imports_topological_order.zipWithIndex.
+ session_background.sessions_structure.imports_topological_order.zipWithIndex.
toMap.withDefaultValue(-1)
val results_json =
@@ -98,7 +98,7 @@
"timing" -> result.timing.json)
})
- if (results.ok) (results_json, results, options, base_info)
+ if (results.ok) (results_json, results, options, session_background)
else {
throw new Server.Error("Session build failed: " + Process_Result.RC.print(results.rc),
results_json)
@@ -127,11 +127,11 @@
progress: Progress = new Progress,
log: Logger = No_Logger
) : (JSON.Object.T, (UUID.T, Headless.Session)) = {
- val (_, _, options, base_info) =
+ val (_, _, options, session_background) =
try { Session_Build.command(args.build, progress = progress) }
catch { case exn: Server.Error => error(exn.message) }
- val resources = Headless.Resources(options, base_info, log = log)
+ val resources = Headless.Resources(options, session_background, log = log)
val session = resources.start_session(print_mode = args.print_mode, progress = progress)
--- a/src/Tools/VSCode/src/build_vscode_extension.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala Fri Dec 16 20:14:41 2022 +0100
@@ -21,7 +21,7 @@
progress: Progress = new Progress
): Unit = {
val keywords =
- Sessions.base_info(options, logic, dirs = dirs).check_errors.base.overall_syntax.keywords
+ Sessions.background(options, logic, dirs = dirs).check_errors.base.overall_syntax.keywords
val output_path = build_dir + Path.explode("isabelle-grammar.json")
progress.echo(output_path.expand.implode)
--- a/src/Tools/VSCode/src/language_server.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Fri Dec 16 20:14:41 2022 +0100
@@ -259,19 +259,20 @@
val try_session =
try {
- val base_info =
- Sessions.base_info(
+ val session_background =
+ Sessions.background(
options, session_name, dirs = session_dirs,
include_sessions = include_sessions, session_ancestor = session_ancestor,
session_requirements = session_requirements).check_errors
def build(no_build: Boolean = false): Build.Results =
Build.build(options,
- selection = Sessions.Selection.session(base_info.session_name),
- build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos)
+ selection = Sessions.Selection.session(session_background.session_name),
+ build_heap = true, no_build = no_build, dirs = session_dirs,
+ infos = session_background.infos)
if (!session_no_build && !build(no_build = true).ok) {
- val start_msg = "Build started for Isabelle/" + base_info.session_name + " ..."
+ val start_msg = "Build started for Isabelle/" + session_background.session_name + " ..."
val fail_msg = "Session build failed -- prover process remains inactive!"
val progress = channel.progress(verbose = true)
@@ -281,7 +282,7 @@
}
val resources =
- new VSCode_Resources(options, base_info, log) {
+ new VSCode_Resources(options, session_background, log) {
override def commit(change: Session.Change): Unit =
if (change.deps_changed || undefined_blobs(change.version).nonEmpty) {
delay_load.invoke()
@@ -291,11 +292,13 @@
val session_options = options.bool("editor_output_state") = true
val session = new Session(session_options, resources)
- Some((base_info, session))
+ Some((session_background, session))
}
catch { case ERROR(msg) => reply_error(msg); None }
- for ((base_info, session) <- try_session) {
+ for ((session_background, session) <- try_session) {
+ val store = Sessions.store(options)
+
session_.change(_ => Some(session))
session.commands_changed += prover_output
@@ -304,9 +307,11 @@
dynamic_output.init()
try {
- Isabelle_Process.start(session, options, base_info.sessions_structure,
- Sessions.store(options), modes = modes, logic = base_info.session_name).await_startup()
- reply_ok("Welcome to Isabelle/" + base_info.session_name + Isabelle_System.isabelle_heading())
+ Isabelle_Process.start(session, options, session_background, store,
+ modes = modes, logic = session_background.session_name).await_startup()
+ reply_ok(
+ "Welcome to Isabelle/" + session_background.session_name +
+ Isabelle_System.isabelle_heading())
}
catch { case ERROR(msg) => reply_error(msg) }
}
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Dec 16 20:14:41 2022 +0100
@@ -69,13 +69,9 @@
class VSCode_Resources(
val options: Options,
- session_base_info: Sessions.Base_Info,
+ session_background: Sessions.Background,
log: Logger = No_Logger)
-extends Resources(
- session_base_info.sessions_structure,
- session_base_info.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_jar.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_jar.scala Fri Dec 16 20:14:41 2022 +0100
@@ -19,10 +19,10 @@
else using(s)(File.read_stream)
}
- object JEdit_Resources extends Scala.Fun_Strings("jEdit.resources") {
+ object JEdit_Resource extends Scala.Fun_Strings("jEdit.resource") {
val here = Scala_Project.here
def apply(args: List[String]): List[String] = args.map(get_resource)
}
- class Scala_Functions extends Scala.Functions(JEdit_Resources)
+ class Scala_Functions extends Scala.Functions(JEdit_Resource)
}
--- a/src/Tools/jEdit/src/jedit_resources.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Fri Dec 16 20:14:41 2022 +0100
@@ -23,14 +23,11 @@
object JEdit_Resources {
def apply(options: Options): JEdit_Resources =
- new JEdit_Resources(JEdit_Sessions.session_base_info(options))
+ new JEdit_Resources(JEdit_Sessions.session_background(options))
}
-class JEdit_Resources private(val session_base_info: Sessions.Base_Info)
-extends Resources(session_base_info.sessions_structure, session_base_info.base) {
- def session_errors: List[String] = session_base_info.errors
-
-
+class JEdit_Resources private(session_background: Sessions.Background)
+extends Resources(session_background) {
/* document node name */
def node_name(path: String): Document.Node.Name =
--- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Dec 16 18:19:23 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Dec 16 20:14:41 2022 +0100
@@ -122,8 +122,8 @@
/* session build process */
- def session_base_info(options: Options): Sessions.Base_Info =
- Sessions.base_info(options,
+ def session_background(options: Options): Sessions.Background =
+ Sessions.background(options,
dirs = JEdit_Sessions.session_dirs,
include_sessions = logic_include_sessions,
session = logic_name(options),
@@ -138,18 +138,18 @@
Build.build(session_options(options),
selection = Sessions.Selection.session(PIDE.resources.session_base.session_name),
progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs,
- infos = PIDE.resources.session_base_info.infos).rc
+ infos = PIDE.resources.session_background.infos).rc
}
def session_start(options0: Options): Unit = {
val session = PIDE.session
val options = session_options(options0)
- val sessions_structure = PIDE.resources.sessions_structure
+ val session_background = PIDE.resources.session_background
val store = Sessions.store(options)
session.phase_changed += PIDE.plugin.session_phase_changed
- Isabelle_Process.start(session, options, sessions_structure, store,
+ Isabelle_Process.start(session, options, session_background, store,
logic = PIDE.resources.session_base.session_name,
modes =
(space_explode(',', options.string("jedit_print_mode")) :::