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)) } }