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