# HG changeset patch
# User wenzelm
# Date 1585308535 -3600
# Node ID d025735a4090e822da92530a5f22556a7db07f77
# Parent  817e26a031987dac6108ac31eda32d098ac8457c
clarified signature;

diff -r 817e26a03198 -r d025735a4090 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Fri Mar 27 12:15:26 2020 +0100
+++ b/src/Pure/PIDE/headless.scala	Fri Mar 27 12:28:55 2020 +0100
@@ -585,7 +585,7 @@
       session.phase_changed += session_phase
 
       progress.echo("Starting session " + session_base_info.session + " ...")
-      Isabelle_Process.start(session, options, session_base_info.sessions_structure,
+      Isabelle_Process(session, options, session_base_info.sessions_structure,
         logic = session_base_info.session, modes = print_mode)
 
       session_error.join match {
diff -r 817e26a03198 -r d025735a4090 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Fri Mar 27 12:15:26 2020 +0100
+++ b/src/Pure/System/isabelle_process.scala	Fri Mar 27 12:28:55 2020 +0100
@@ -12,7 +12,7 @@
 
 object Isabelle_Process
 {
-  def start(
+  def apply(
     session: Session,
     options: Options,
     sessions_structure: Sessions.Structure,
@@ -24,26 +24,6 @@
     store: Option[Sessions.Store] = None,
     phase_changed: Session.Phase => Unit = null)
   {
-    if (phase_changed != null)
-      session.phase_changed += Session.Consumer("Isabelle_Process")(phase_changed)
-
-    session.start(receiver =>
-      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,
-    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(),
-    store: Option[Sessions.Store] = None): Prover =
-  {
     val channel = System_Channel()
     val process =
       try {
@@ -57,6 +37,9 @@
       catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
     process.stdin.close
 
-    new Prover(receiver, xml_cache, channel, process)
+    if (phase_changed != null)
+      session.phase_changed += Session.Consumer("Isabelle_Process")(phase_changed)
+
+    session.start(receiver => new Prover(receiver, session.xml_cache, channel, process))
   }
 }
diff -r 817e26a03198 -r d025735a4090 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Mar 27 12:15:26 2020 +0100
+++ b/src/Pure/Tools/build.scala	Fri Mar 27 12:28:55 2020 +0100
@@ -250,7 +250,7 @@
 
           val session_result = Future.promise[Process_Result]
 
-          Isabelle_Process.start(session, options, sessions_structure,
+          Isabelle_Process(session, options, sessions_structure,
             logic = parent, cwd = info.dir.file, env = env, store = Some(store),
             phase_changed =
             {
diff -r 817e26a03198 -r d025735a4090 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Fri Mar 27 12:15:26 2020 +0100
+++ b/src/Tools/VSCode/src/server.scala	Fri Mar 27 12:28:55 2020 +0100
@@ -318,7 +318,7 @@
         }
       session.phase_changed += session_phase
 
-      Isabelle_Process.start(
+      Isabelle_Process(
         session, options, base_info.sessions_structure, modes = modes, logic = base_info.session)
     }
   }
diff -r 817e26a03198 -r d025735a4090 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Mar 27 12:15:26 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Mar 27 12:28:55 2020 +0100
@@ -137,7 +137,7 @@
   {
     val options = session_options(options0)
 
-    Isabelle_Process.start(PIDE.session, options,
+    Isabelle_Process(PIDE.session, options,
       PIDE.resources.session_base_info.sessions_structure,
       logic = PIDE.resources.session_name,
       store = Some(Sessions.store(options)),