--- a/src/Pure/PIDE/headless.scala Sat Mar 28 17:27:01 2020 +0000
+++ b/src/Pure/PIDE/headless.scala Sat Mar 28 17:27:08 2020 +0000
@@ -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).await_startup
- session_error.join match {
- case "" => session
- case msg => session.stop(); error(msg)
- }
+ session
}
--- a/src/Pure/PIDE/session.scala Sat Mar 28 17:27:01 2020 +0000
+++ b/src/Pure/PIDE/session.scala Sat Mar 28 17:27:08 2020 +0000
@@ -566,15 +566,15 @@
//{{{
arg match {
case output: Prover.Output =>
- if (output.is_stdout || output.is_stderr)
- raw_output_messages.post(output)
- else handle_output(output)
-
if (output.is_syslog) {
syslog += output.message
syslog_messages.post(output)
}
+ if (output.is_stdout || output.is_stderr)
+ raw_output_messages.post(output)
+ else handle_output(output)
+
all_messages.post(output)
case input: Prover.Input =>
--- a/src/Pure/System/isabelle_process.scala Sat Mar 28 17:27:01 2020 +0000
+++ b/src/Pure/System/isabelle_process.scala Sat Mar 28 17:27:08 2020 +0000
@@ -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,36 @@
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 = Future.promise[String]
+ private val terminated = Future.promise[Process_Result]
+
+ session.phase_changed +=
+ Session.Consumer(getClass.getName) {
+ case Session.Ready =>
+ startup.fulfill("")
+ case Session.Terminated(result) =>
+ if (!result.ok && !startup.is_finished) {
+ val syslog = session.syslog_content()
+ val err = "Session startup failed" + (if (syslog.isEmpty) "" else ":\n" + syslog)
+ startup.fulfill(err)
+ }
+ terminated.fulfill(result)
+ case _ =>
+ }
+
+ session.start(receiver => new Prover(receiver, session.xml_cache, channel, process))
+
+ def await_startup(): Isabelle_Process =
+ startup.join match {
+ case "" => this
+ case err => session.stop(); error(err)
+ }
+
+ def join(): Process_Result = terminated.join
+}
\ No newline at end of file
--- a/src/Pure/Tools/build.scala Sat Mar 28 17:27:01 2020 +0000
+++ b/src/Pure/Tools/build.scala Sat Mar 28 17:27:08 2020 +0000
@@ -248,18 +248,13 @@
val handler = new Handler(progress, session, name)
session.init_protocol_handler(handler)
- val session_result = Future.promise[Process_Result]
+ val process =
+ Isabelle_Process(session, options, sessions_structure, store,
+ logic = parent, cwd = info.dir.file, env = env).await_startup
- 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 _ =>
- })
+ session.protocol_command("build_session", args_yxml)
- val result = session_result.join
+ val result = process.join
handler.result_error.join match {
case "" => result
case msg =>
--- a/src/Tools/VSCode/src/server.scala Sat Mar 28 17:27:01 2020 +0000
+++ b/src/Tools/VSCode/src/server.scala Sat Mar 28 17:27:08 2020 +0000
@@ -305,22 +305,12 @@
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)
+ try {
+ Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options),
+ modes = modes, logic = base_info.session).await_startup
+ 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 Sat Mar 28 17:27:01 2020 +0000
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Sat Mar 28 17:27:08 2020 +0000
@@ -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 Sat Mar 28 17:27:01 2020 +0000
+++ b/src/Tools/jEdit/src/plugin.scala Sat Mar 28 17:27:08 2020 +0000
@@ -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 {