--- a/src/Pure/PIDE/session.scala Thu Apr 24 22:41:03 2014 +0200
+++ b/src/Pure/PIDE/session.scala Thu Apr 24 23:02:10 2014 +0200
@@ -265,6 +265,7 @@
/* internal messages */
private case class Start(name: String, args: List[String])
+ private case object Stop
private case class Cancel_Exec(exec_id: Document_ID.Exec)
private case class Protocol_Command(name: String, args: List[String])
private case class Messages(msgs: List[Prover.Message])
@@ -305,7 +306,7 @@
private val timer = new Timer("receiver", true)
timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
- def cancel() { timer.cancel() }
+ def shutdown() { timer.cancel(); flush() }
}
@@ -482,72 +483,69 @@
/* main thread */
- Consumer_Thread.fork[Any]("manager", daemon = true)(
- consume = (arg: Any) =>
- {
- //{{{
- arg match {
- case Start(name, args) if prover.isEmpty =>
- if (phase == Session.Inactive || phase == Session.Failed) {
- phase = Session.Startup
- prover = Some(resources.start_prover(receiver.invoke _, name, args))
- }
+ Consumer_Thread.fork[Any]("manager", daemon = true)
+ {
+ case arg: Any =>
+ //{{{
+ arg match {
+ case Start(name, args) if prover.isEmpty =>
+ if (phase == Session.Inactive || phase == Session.Failed) {
+ phase = Session.Startup
+ prover = Some(resources.start_prover(receiver.invoke _, name, args))
+ }
- case Update_Options(options) =>
- if (prover.isDefined && is_ready) {
- prover.get.options(options)
- handle_raw_edits(Document.Blobs.empty, Nil)
- }
- global_options.event(Session.Global_Options(options))
-
- case Cancel_Exec(exec_id) if prover.isDefined =>
- prover.get.cancel_exec(exec_id)
+ case Stop =>
+ if (phase == Session.Ready) {
+ _protocol_handlers = _protocol_handlers.stop(prover.get)
+ global_state.change(_ => Document.State.init) // FIXME event bus!?
+ phase = Session.Shutdown
+ prover.get.terminate
+ prover = None
+ phase = Session.Inactive
+ }
- case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
- handle_raw_edits(doc_blobs, edits)
+ case Update_Options(options) =>
+ if (prover.isDefined && is_ready) {
+ prover.get.options(options)
+ handle_raw_edits(Document.Blobs.empty, Nil)
+ }
+ global_options.event(Session.Global_Options(options))
- case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
- prover.get.dialog_result(serial, result)
- handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
-
- case Protocol_Command(name, args) if prover.isDefined =>
- prover.get.protocol_command(name, args:_*)
+ case Cancel_Exec(exec_id) if prover.isDefined =>
+ prover.get.cancel_exec(exec_id)
- case Messages(msgs) =>
- msgs foreach {
- case input: Prover.Input =>
- all_messages.event(input)
+ case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
+ handle_raw_edits(doc_blobs, edits)
+
+ case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
+ prover.get.dialog_result(serial, result)
+ handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
- case output: Prover.Output =>
- if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
- else handle_output(output)
- if (output.is_syslog) syslog_messages.event(output)
- all_messages.event(output)
- }
+ case Protocol_Command(name, args) if prover.isDefined =>
+ prover.get.protocol_command(name, args:_*)
- case change: Session.Change if prover.isDefined =>
- if (global_state.value.is_assigned(change.previous))
- handle_change(change)
- else postponed_changes.store(change)
+ case Messages(msgs) =>
+ msgs foreach {
+ case input: Prover.Input =>
+ all_messages.event(input)
- case bad => System.err.println("Session.manager: ignoring bad message " + bad)
- }
- true
- //}}}
- },
- finish = () =>
- {
- if (phase == Session.Ready) {
- _protocol_handlers = _protocol_handlers.stop(prover.get)
- global_state.change(_ => Document.State.init) // FIXME event bus!?
- phase = Session.Shutdown
- prover.get.terminate
- prover = None
- phase = Session.Inactive
- }
- receiver.cancel()
+ case output: Prover.Output =>
+ if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
+ else handle_output(output)
+ if (output.is_syslog) syslog_messages.event(output)
+ all_messages.event(output)
+ }
+
+ case change: Session.Change if prover.isDefined =>
+ if (global_state.value.is_assigned(change.previous))
+ handle_change(change)
+ else postponed_changes.store(change)
+
+ case bad => System.err.println("Session.manager: ignoring bad message " + bad)
}
- )
+ true
+ //}}}
+ }
}
@@ -558,6 +556,8 @@
def stop()
{
+ manager.send_wait(Stop)
+ receiver.shutdown()
change_parser.shutdown()
change_buffer.shutdown()
manager.shutdown()