# HG changeset patch
# User wenzelm
# Date 1622839571 -7200
# Node ID 8d9ac6cfc270dcb8940f77dd7c494918b02a56d7
# Parent  e67c951f1c186a06cac7e058a255b980eb6548ea
clarified signature;

diff -r e67c951f1c18 -r 8d9ac6cfc270 src/Pure/PIDE/headless.scala
--- 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
diff -r e67c951f1c18 -r 8d9ac6cfc270 src/Pure/System/isabelle_process.scala
--- 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
diff -r e67c951f1c18 -r 8d9ac6cfc270 src/Pure/Tools/build_job.scala
--- 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)
diff -r e67c951f1c18 -r 8d9ac6cfc270 src/Tools/VSCode/src/language_server.scala
--- 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) }
diff -r e67c951f1c18 -r 8d9ac6cfc270 src/Tools/jEdit/src/jedit_sessions.scala
--- 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")) :::