--- a/src/Pure/ML/ml_console.scala Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Pure/ML/ml_console.scala Fri Mar 27 12:03:20 2020 +0100
@@ -50,6 +50,8 @@
if (more_args.nonEmpty) getopts.usage()
+ val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+
// build logic
if (!no_build && !raw_ml_system) {
val progress = new Console_Progress()
@@ -62,7 +64,7 @@
// process loop
val process =
- ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
+ ML_Process(options, sessions_structure, 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)),
--- a/src/Pure/ML/ml_process.scala Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Pure/ML/ml_process.scala Fri Mar 27 12:03:20 2020 +0100
@@ -13,29 +13,25 @@
object ML_Process
{
def apply(options: Options,
+ sessions_structure: Sessions.Structure,
logic: String = "",
args: List[String] = Nil,
- dirs: List[Path] = Nil,
modes: List[String] = Nil,
raw_ml_system: Boolean = false,
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
cleanup: () => Unit = () => (),
- sessions_structure: Option[Sessions.Structure] = None,
session_base: Option[Sessions.Base] = None,
store: Option[Sessions.Store] = None): Bash.Process =
{
val logic_name = Isabelle_System.default_logic(logic)
val _store = store.getOrElse(Sessions.store(options))
- val sessions_structure1 =
- sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
-
val heaps: List[String] =
if (raw_ml_system) Nil
else {
- sessions_structure1.selection(Sessions.Selection.session(logic_name)).
+ sessions_structure.selection(Sessions.Selection.session(logic_name)).
build_requirements(List(logic_name)).
map(a => File.platform_path(_store.the_heap(a)))
}
@@ -96,8 +92,8 @@
ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
List("Resources.init_session_base" +
- " {session_positions = " + print_sessions(sessions_structure1.session_positions) +
- ", session_directories = " + print_table(sessions_structure1.dest_session_directories) +
+ " {session_positions = " + print_sessions(sessions_structure.session_positions) +
+ ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
", docs = " + print_list(base.doc_names) +
", global_theories = " + print_table(base.global_theories.toList) +
", loaded_theories = " + print_list(base.loaded_theories.keys) + "}")
@@ -182,8 +178,11 @@
val more_args = getopts(args)
if (args.isEmpty || more_args.nonEmpty) getopts.usage()
- val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
- result().print_stdout.rc
+ val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+
+ val rc =
+ ML_Process(options, sessions_structure, logic = logic, args = eval_args, modes = modes)
+ .result().print_stdout.rc
sys.exit(rc)
})
}
--- a/src/Pure/PIDE/headless.scala Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Pure/PIDE/headless.scala Fri Mar 27 12:03:20 2020 +0100
@@ -584,9 +584,11 @@
}
session.phase_changed += session_phase
+ val sessions_structure = Sessions.load_structure(options, dirs = session_base_info.dirs)
+
progress.echo("Starting session " + session_base_info.session + " ...")
- Isabelle_Process.start(session, options,
- logic = session_base_info.session, dirs = session_base_info.dirs, modes = print_mode)
+ Isabelle_Process.start(session, options, sessions_structure,
+ logic = session_base_info.session, modes = print_mode)
session_error.join match {
case "" => session
--- a/src/Pure/System/isabelle_process.scala Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Pure/System/isabelle_process.scala Fri Mar 27 12:03:20 2020 +0100
@@ -12,15 +12,15 @@
object Isabelle_Process
{
- def start(session: Session,
+ def start(
+ session: Session,
options: Options,
+ sessions_structure: Sessions.Structure,
logic: String = "",
args: List[String] = Nil,
- dirs: List[Path] = Nil,
modes: List[String] = Nil,
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
- sessions_structure: Option[Sessions.Structure] = None,
store: Option[Sessions.Store] = None,
phase_changed: Session.Phase => Unit = null)
{
@@ -28,22 +28,20 @@
session.phase_changed += Session.Consumer("Isabelle_Process")(phase_changed)
session.start(receiver =>
- Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
- cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache,
- sessions_structure = sessions_structure, store = store))
+ Isabelle_Process(options, sessions_structure, logic = logic, args = args, modes = modes,
+ cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache, store = store))
}
def apply(
options: Options,
+ sessions_structure: Sessions.Structure,
logic: String = "",
args: List[String] = Nil,
- dirs: List[Path] = Nil,
modes: List[String] = Nil,
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true),
xml_cache: XML.Cache = XML.make_cache(),
- sessions_structure: Option[Sessions.Structure] = None,
store: Option[Sessions.Store] = None): Prover =
{
val channel = System_Channel()
@@ -52,8 +50,9 @@
val channel_options =
options.string.update("system_channel_address", channel.address).
string.update("system_channel_password", channel.password)
- ML_Process(channel_options, logic = logic, args = args, dirs = dirs, modes = modes,
- cwd = cwd, env = env, sessions_structure = sessions_structure, store = store)
+ ML_Process(
+ channel_options, sessions_structure, logic = logic, args = args, modes = modes,
+ cwd = cwd, env = env, store = store)
}
catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
process.stdin.close
--- a/src/Pure/Tools/build.scala Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Pure/Tools/build.scala Fri Mar 27 12:03:20 2020 +0100
@@ -250,8 +250,8 @@
val session_result = Future.promise[Process_Result]
- Isabelle_Process.start(session, options, logic = parent, cwd = info.dir.file, env = env,
- sessions_structure = Some(sessions_structure), store = Some(store),
+ Isabelle_Process.start(session, options, sessions_structure,
+ logic = parent, cwd = info.dir.file, env = env, store = Some(store),
phase_changed =
{
case Session.Ready => session.protocol_command("build_session", args_yxml)
@@ -280,16 +280,16 @@
val process =
if (Sessions.is_pure(name)) {
- ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
+ ML_Process(options, deps.sessions_structure, raw_ml_system = true,
+ cwd = info.dir.file, env = env, store = Some(store),
args =
(for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
List("--eval", eval),
- env = env, sessions_structure = Some(deps.sessions_structure), store = Some(store),
cleanup = () => args_file.delete)
}
else {
- ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
- env = env, sessions_structure = Some(deps.sessions_structure), store = Some(store),
+ ML_Process(options, deps.sessions_structure, parent, List("--eval", eval),
+ cwd = info.dir.file, env = env, store = Some(store),
cleanup = () => args_file.delete)
}
--- a/src/Tools/VSCode/src/server.scala Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Tools/VSCode/src/server.scala Fri Mar 27 12:03:20 2020 +0100
@@ -318,8 +318,8 @@
}
session.phase_changed += session_phase
- Isabelle_Process.start(session, options, modes = modes,
- sessions_structure = Some(base_info.sessions_structure), logic = base_info.session)
+ Isabelle_Process.start(
+ session, options, base_info.sessions_structure, modes = modes, logic = base_info.session)
}
}
--- a/src/Tools/jEdit/src/jedit_sessions.scala Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Mar 27 12:03:20 2020 +0100
@@ -138,7 +138,7 @@
val options = session_options(options0)
Isabelle_Process.start(PIDE.session, options,
- sessions_structure = Some(PIDE.resources.session_base_info.sessions_structure),
+ PIDE.resources.session_base_info.sessions_structure,
logic = PIDE.resources.session_name,
store = Some(Sessions.store(options)),
modes =