src/Pure/System/isabelle_process.scala
changeset 71597 d025735a4090
parent 71594 8a298184f3f9
child 71598 269dc4bf1f40
--- 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))
   }
 }