--- 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 {
--- 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))
}
}
--- 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 =
{
--- 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)
}
}
--- 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)),