--- a/src/Pure/ML/ml_console.scala Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Pure/ML/ml_console.scala Fri Mar 27 12:46:56 2020 +0100
@@ -51,6 +51,7 @@
val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+ val store = Sessions.store(options)
// build logic
if (!no_build && !raw_ml_system) {
@@ -64,10 +65,10 @@
// process loop
val process =
- ML_Process(options, sessions_structure, logic = logic, args = List("-i"), redirect = true,
+ ML_Process(options, sessions_structure, store,
+ logic = logic, args = List("-i"), redirect = true,
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
raw_ml_system = raw_ml_system,
- store = Some(Sessions.store(options)),
session_base =
if (raw_ml_system) None
else Some(Sessions.base_info(
--- a/src/Pure/ML/ml_process.scala Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Pure/ML/ml_process.scala Fri Mar 27 12:46:56 2020 +0100
@@ -14,6 +14,7 @@
{
def apply(options: Options,
sessions_structure: Sessions.Structure,
+ store: Sessions.Store,
logic: String = "",
args: List[String] = Nil,
modes: List[String] = Nil,
@@ -22,18 +23,16 @@
env: Map[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
cleanup: () => Unit = () => (),
- session_base: Option[Sessions.Base] = None,
- store: Option[Sessions.Store] = None): Bash.Process =
+ session_base: Option[Sessions.Base] = None): Bash.Process =
{
val logic_name = Isabelle_System.default_logic(logic)
- val _store = store.getOrElse(Sessions.store(options))
val heaps: List[String] =
if (raw_ml_system) Nil
else {
sessions_structure.selection(Sessions.Selection.session(logic_name)).
build_requirements(List(logic_name)).
- map(a => File.platform_path(_store.the_heap(a)))
+ map(a => File.platform_path(store.the_heap(a)))
}
val eval_init =
@@ -179,9 +178,10 @@
if (args.isEmpty || more_args.nonEmpty) getopts.usage()
val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+ val store = Sessions.store(options)
val rc =
- ML_Process(options, sessions_structure, logic = logic, args = eval_args, modes = modes)
+ ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes)
.result().print_stdout.rc
sys.exit(rc)
})
--- a/src/Pure/PIDE/headless.scala Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Pure/PIDE/headless.scala Fri Mar 27 12:46:56 2020 +0100
@@ -585,7 +585,8 @@
session.phase_changed += session_phase
progress.echo("Starting session " + session_base_info.session + " ...")
- Isabelle_Process(session, options, session_base_info.sessions_structure,
+ val store = Sessions.store(options)
+ Isabelle_Process(session, options, session_base_info.sessions_structure, store,
logic = session_base_info.session, modes = print_mode)
session_error.join match {
--- a/src/Pure/System/isabelle_process.scala Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Pure/System/isabelle_process.scala Fri Mar 27 12:46:56 2020 +0100
@@ -16,12 +16,12 @@
session: Session,
options: Options,
sessions_structure: Sessions.Structure,
+ store: Sessions.Store,
logic: String = "",
args: List[String] = Nil,
modes: List[String] = Nil,
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
- store: Option[Sessions.Store] = None,
phase_changed: Session.Phase => Unit = null)
{
val channel = System_Channel()
@@ -30,9 +30,8 @@
val channel_options =
options.string.update("system_channel_address", channel.address).
string.update("system_channel_password", channel.password)
- ML_Process(
- channel_options, sessions_structure, logic = logic, args = args, modes = modes,
- cwd = cwd, env = env, store = store)
+ ML_Process(channel_options, sessions_structure, store,
+ logic = logic, args = args, modes = modes, cwd = cwd, env = env)
}
catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
process.stdin.close
--- a/src/Pure/Tools/build.scala Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Pure/Tools/build.scala Fri Mar 27 12:46:56 2020 +0100
@@ -250,8 +250,8 @@
val session_result = Future.promise[Process_Result]
- Isabelle_Process(session, options, sessions_structure,
- logic = parent, cwd = info.dir.file, env = env, store = Some(store),
+ Isabelle_Process(session, options, sessions_structure, store,
+ logic = parent, cwd = info.dir.file, env = env,
phase_changed =
{
case Session.Ready => session.protocol_command("build_session", args_yxml)
@@ -280,17 +280,16 @@
val process =
if (Sessions.is_pure(name)) {
- ML_Process(options, deps.sessions_structure, raw_ml_system = true,
+ ML_Process(options, deps.sessions_structure, store, raw_ml_system = true,
args =
(for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
List("--eval", eval),
- cwd = info.dir.file, env = env, store = Some(store),
- cleanup = () => args_file.delete)
+ cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
}
else {
- ML_Process(options, deps.sessions_structure, logic = parent, args = List("--eval", eval),
- cwd = info.dir.file, env = env, store = Some(store),
- cleanup = () => args_file.delete)
+ ML_Process(options, deps.sessions_structure, store, logic = parent,
+ args = List("--eval", eval),
+ cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
}
process.result(
--- a/src/Tools/VSCode/src/server.scala Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Tools/VSCode/src/server.scala Fri Mar 27 12:46:56 2020 +0100
@@ -318,8 +318,9 @@
}
session.phase_changed += session_phase
- Isabelle_Process(
- session, options, base_info.sessions_structure, modes = modes, logic = base_info.session)
+ val store = Sessions.store(options)
+ Isabelle_Process(session, options, base_info.sessions_structure, store,
+ modes = modes, logic = base_info.session)
}
}
--- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Mar 27 12:46:56 2020 +0100
@@ -136,11 +136,11 @@
def session_start(options0: Options)
{
val options = session_options(options0)
+ val store = Sessions.store(options)
Isabelle_Process(PIDE.session, options,
- PIDE.resources.session_base_info.sessions_structure,
+ PIDE.resources.session_base_info.sessions_structure, store,
logic = PIDE.resources.session_name,
- store = Some(Sessions.store(options)),
modes =
(space_explode(',', options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,