--- a/src/Pure/PIDE/headless.scala Fri Mar 27 22:06:46 2020 +0100
+++ b/src/Pure/PIDE/headless.scala Sat Mar 28 12:06:37 2020 +0100
@@ -571,28 +571,11 @@
{
val session = new Session(session_base_info.session, options, resources)
- val session_error = Future.promise[String]
- var session_phase: Session.Consumer[Session.Phase] = null
- session_phase =
- Session.Consumer(getClass.getName) {
- case Session.Ready =>
- session.phase_changed -= session_phase
- session_error.fulfill("")
- case Session.Terminated(result) if !result.ok =>
- session.phase_changed -= session_phase
- session_error.fulfill("Session start failed: return code " + result.rc)
- case _ =>
- }
- session.phase_changed += session_phase
-
progress.echo("Starting session " + session_base_info.session + " ...")
Isabelle_Process(session, options, session_base_info.sessions_structure, store,
- logic = session_base_info.session, modes = print_mode)
+ logic = session_base_info.session, modes = print_mode).startup_join()
- session_error.join match {
- case "" => session
- case msg => session.stop(); error(msg)
- }
+ session
}
--- a/src/Pure/System/isabelle_process.scala Fri Mar 27 22:06:46 2020 +0100
+++ b/src/Pure/System/isabelle_process.scala Sat Mar 28 12:06:37 2020 +0100
@@ -21,8 +21,7 @@
args: List[String] = Nil,
modes: List[String] = Nil,
cwd: JFile = null,
- env: Map[String, String] = Isabelle_System.settings(),
- phase_changed: Session.Phase => Unit = null)
+ env: Map[String, String] = Isabelle_System.settings()): Isabelle_Process =
{
val channel = System_Channel()
val process =
@@ -36,9 +35,28 @@
catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
process.stdin.close
- if (phase_changed != null)
- session.phase_changed += Session.Consumer("Isabelle_Process")(phase_changed)
-
- session.start(receiver => new Prover(receiver, session.xml_cache, channel, process))
+ new Isabelle_Process(session, channel, process)
}
}
+
+class Isabelle_Process private(session: Session, channel: System_Channel, process: Bash.Process)
+{
+ private val startup_error = Future.promise[String]
+
+ session.phase_changed +=
+ Session.Consumer(getClass.getName) {
+ case Session.Ready =>
+ startup_error.fulfill("")
+ case Session.Terminated(result) if !result.ok && !startup_error.is_finished =>
+ startup_error.fulfill("Session start failed: return code " + result.rc)
+ case _ =>
+ }
+
+ def startup_join(): Unit =
+ startup_error.join match {
+ case "" =>
+ case msg => session.stop(); error(msg)
+ }
+
+ session.start(receiver => new Prover(receiver, session.xml_cache, channel, process))
+}
\ No newline at end of file
--- a/src/Pure/Tools/build.scala Fri Mar 27 22:06:46 2020 +0100
+++ b/src/Pure/Tools/build.scala Sat Mar 28 12:06:37 2020 +0100
@@ -249,15 +249,14 @@
session.init_protocol_handler(handler)
val session_result = Future.promise[Process_Result]
-
+ session.phase_changed += Session.Consumer("build_session")
+ {
+ case Session.Ready => session.protocol_command("build_session", args_yxml)
+ case Session.Terminated(result) => session_result.fulfill(result)
+ case _ =>
+ }
Isabelle_Process(session, options, sessions_structure, store,
- logic = parent, cwd = info.dir.file, env = env,
- phase_changed =
- {
- case Session.Ready => session.protocol_command("build_session", args_yxml)
- case Session.Terminated(result) => session_result.fulfill(result)
- case _ =>
- })
+ logic = parent, cwd = info.dir.file, env = env)
val result = session_result.join
handler.result_error.join match {
--- a/src/Tools/VSCode/src/server.scala Fri Mar 27 22:06:46 2020 +0100
+++ b/src/Tools/VSCode/src/server.scala Sat Mar 28 12:06:37 2020 +0100
@@ -305,22 +305,14 @@
dynamic_output.init()
- var session_phase: Session.Consumer[Session.Phase] = null
- session_phase =
- Session.Consumer(getClass.getName) {
- case Session.Ready =>
- session.phase_changed -= session_phase
- reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")")
- case Session.Terminated(result) if !result.ok =>
- session.phase_changed -= session_phase
- reply_error("Prover startup failed: return code " + result.rc)
- case _ =>
- }
- session.phase_changed += session_phase
-
- val store = Sessions.store(options)
- Isabelle_Process(session, options, base_info.sessions_structure, store,
- modes = modes, logic = base_info.session)
+ val process =
+ Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options),
+ modes = modes, logic = base_info.session)
+ try {
+ process.startup_join()
+ reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")")
+ }
+ catch { case ERROR(msg) => reply_error(msg) }
}
}
--- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Mar 27 22:06:46 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Sat Mar 28 12:06:37 2020 +0100
@@ -135,15 +135,17 @@
def session_start(options0: Options)
{
+ val session = PIDE.session
val options = session_options(options0)
+ val sessions_structure = PIDE.resources.session_base_info.sessions_structure
val store = Sessions.store(options)
- Isabelle_Process(PIDE.session, options,
- PIDE.resources.session_base_info.sessions_structure, store,
+ session.phase_changed += PIDE.plugin.session_phase_changed
+
+ Isabelle_Process(session, options, sessions_structure, store,
logic = PIDE.resources.session_name,
modes =
(space_explode(',', options.string("jedit_print_mode")) :::
- space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,
- phase_changed = PIDE.plugin.session_phase_changed)
+ space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse)
}
}
--- a/src/Tools/jEdit/src/plugin.scala Fri Mar 27 22:06:46 2020 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Sat Mar 28 12:06:37 2020 +0100
@@ -189,7 +189,7 @@
/* session phase */
- val session_phase_changed: Session.Phase => Unit =
+ val session_phase_changed: Session.Consumer[Session.Phase] = Session.Consumer("Isabelle/jEdit")
{
case Session.Terminated(result) if !result.ok =>
GUI_Thread.later {