--- a/src/Pure/PIDE/headless.scala Fri Jun 04 22:30:17 2021 +0200
+++ b/src/Pure/PIDE/headless.scala Fri Jun 04 22:46:11 2021 +0200
@@ -574,7 +574,7 @@
val session = new Session(session_base_info.session, options, resources)
progress.echo("Starting session " + session_base_info.session + " ...")
- Isabelle_Process(session, options, session_base_info.sessions_structure, store,
+ Isabelle_Process.start(session, options, session_base_info.sessions_structure, store,
logic = session_base_info.session, modes = print_mode).await_startup()
session
--- a/src/Pure/System/isabelle_process.scala Fri Jun 04 22:30:17 2021 +0200
+++ b/src/Pure/System/isabelle_process.scala Fri Jun 04 22:46:11 2021 +0200
@@ -12,7 +12,7 @@
object Isabelle_Process
{
- def apply(
+ def start(
session: Session,
options: Options,
sessions_structure: Sessions.Structure,
@@ -39,11 +39,14 @@
catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
process.stdin.close()
- new Isabelle_Process(session, channel, process)
+ val isabelle_process = new Isabelle_Process(session, process)
+ session.start(receiver => new Prover(receiver, session.cache, channel, process))
+
+ isabelle_process
}
}
-class Isabelle_Process private(session: Session, channel: System_Channel, process: Bash.Process)
+class Isabelle_Process private(session: Session, process: Bash.Process)
{
private val startup = Future.promise[String]
private val terminated = Future.promise[Process_Result]
@@ -62,8 +65,6 @@
case _ =>
}
- session.start(receiver => new Prover(receiver, session.cache, channel, process))
-
def await_startup(): Isabelle_Process =
startup.join match {
case "" => this
--- a/src/Pure/Tools/build_job.scala Fri Jun 04 22:30:17 2021 +0200
+++ b/src/Pure/Tools/build_job.scala Fri Jun 04 22:46:11 2021 +0200
@@ -414,7 +414,7 @@
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
val process =
- Isabelle_Process(session, options, sessions_structure, store,
+ Isabelle_Process.start(session, options, sessions_structure, store,
logic = parent, raw_ml_system = is_pure,
use_prelude = use_prelude, eval_main = eval_main,
cwd = info.dir.file, env = env)
--- a/src/Tools/VSCode/src/language_server.scala Fri Jun 04 22:30:17 2021 +0200
+++ b/src/Tools/VSCode/src/language_server.scala Fri Jun 04 22:46:11 2021 +0200
@@ -306,8 +306,8 @@
dynamic_output.init()
try {
- Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options),
- modes = modes, logic = base_info.session).await_startup()
+ Isabelle_Process.start(session, options, base_info.sessions_structure,
+ Sessions.store(options), modes = modes, logic = base_info.session).await_startup()
reply_ok("Welcome to Isabelle/" + base_info.session + Isabelle_System.isabelle_heading())
}
catch { case ERROR(msg) => reply_error(msg) }
--- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Jun 04 22:30:17 2021 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Jun 04 22:46:11 2021 +0200
@@ -143,7 +143,7 @@
session.phase_changed += PIDE.plugin.session_phase_changed
- Isabelle_Process(session, options, sessions_structure, store,
+ Isabelle_Process.start(session, options, sessions_structure, store,
logic = PIDE.resources.session_name,
modes =
(space_explode(',', options.string("jedit_print_mode")) :::