more careful shutdown (amending f2f53f7046f4);
authorwenzelm
Thu Apr 24 23:02:10 2014 +0200 (2014-04-24)
changeset 56709e83356e94380
parent 56708 d39148de6eee
child 56710 8f102c18eab7
more careful shutdown (amending f2f53f7046f4);
src/Pure/PIDE/session.scala
     1.1 --- a/src/Pure/PIDE/session.scala	Thu Apr 24 22:41:03 2014 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Thu Apr 24 23:02:10 2014 +0200
     1.3 @@ -265,6 +265,7 @@
     1.4    /* internal messages */
     1.5  
     1.6    private case class Start(name: String, args: List[String])
     1.7 +  private case object Stop
     1.8    private case class Cancel_Exec(exec_id: Document_ID.Exec)
     1.9    private case class Protocol_Command(name: String, args: List[String])
    1.10    private case class Messages(msgs: List[Prover.Message])
    1.11 @@ -305,7 +306,7 @@
    1.12      private val timer = new Timer("receiver", true)
    1.13      timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
    1.14  
    1.15 -    def cancel() { timer.cancel() }
    1.16 +    def shutdown() { timer.cancel(); flush() }
    1.17    }
    1.18  
    1.19  
    1.20 @@ -482,72 +483,69 @@
    1.21  
    1.22      /* main thread */
    1.23  
    1.24 -    Consumer_Thread.fork[Any]("manager", daemon = true)(
    1.25 -      consume = (arg: Any) =>
    1.26 -        {
    1.27 -          //{{{
    1.28 -          arg match {
    1.29 -            case Start(name, args) if prover.isEmpty =>
    1.30 -              if (phase == Session.Inactive || phase == Session.Failed) {
    1.31 -                phase = Session.Startup
    1.32 -                prover = Some(resources.start_prover(receiver.invoke _, name, args))
    1.33 -              }
    1.34 +    Consumer_Thread.fork[Any]("manager", daemon = true)
    1.35 +    {
    1.36 +      case arg: Any =>
    1.37 +        //{{{
    1.38 +        arg match {
    1.39 +          case Start(name, args) if prover.isEmpty =>
    1.40 +            if (phase == Session.Inactive || phase == Session.Failed) {
    1.41 +              phase = Session.Startup
    1.42 +              prover = Some(resources.start_prover(receiver.invoke _, name, args))
    1.43 +            }
    1.44  
    1.45 -            case Update_Options(options) =>
    1.46 -              if (prover.isDefined && is_ready) {
    1.47 -                prover.get.options(options)
    1.48 -                handle_raw_edits(Document.Blobs.empty, Nil)
    1.49 -              }
    1.50 -              global_options.event(Session.Global_Options(options))
    1.51 -
    1.52 -            case Cancel_Exec(exec_id) if prover.isDefined =>
    1.53 -              prover.get.cancel_exec(exec_id)
    1.54 +          case Stop =>
    1.55 +            if (phase == Session.Ready) {
    1.56 +              _protocol_handlers = _protocol_handlers.stop(prover.get)
    1.57 +              global_state.change(_ => Document.State.init)  // FIXME event bus!?
    1.58 +              phase = Session.Shutdown
    1.59 +              prover.get.terminate
    1.60 +              prover = None
    1.61 +              phase = Session.Inactive
    1.62 +            }
    1.63  
    1.64 -            case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
    1.65 -              handle_raw_edits(doc_blobs, edits)
    1.66 +          case Update_Options(options) =>
    1.67 +            if (prover.isDefined && is_ready) {
    1.68 +              prover.get.options(options)
    1.69 +              handle_raw_edits(Document.Blobs.empty, Nil)
    1.70 +            }
    1.71 +            global_options.event(Session.Global_Options(options))
    1.72  
    1.73 -            case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
    1.74 -              prover.get.dialog_result(serial, result)
    1.75 -              handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
    1.76 -
    1.77 -            case Protocol_Command(name, args) if prover.isDefined =>
    1.78 -              prover.get.protocol_command(name, args:_*)
    1.79 +          case Cancel_Exec(exec_id) if prover.isDefined =>
    1.80 +            prover.get.cancel_exec(exec_id)
    1.81  
    1.82 -            case Messages(msgs) =>
    1.83 -              msgs foreach {
    1.84 -                case input: Prover.Input =>
    1.85 -                  all_messages.event(input)
    1.86 +          case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
    1.87 +            handle_raw_edits(doc_blobs, edits)
    1.88 +
    1.89 +          case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
    1.90 +            prover.get.dialog_result(serial, result)
    1.91 +            handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
    1.92  
    1.93 -                case output: Prover.Output =>
    1.94 -                  if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
    1.95 -                  else handle_output(output)
    1.96 -                  if (output.is_syslog) syslog_messages.event(output)
    1.97 -                  all_messages.event(output)
    1.98 -              }
    1.99 +          case Protocol_Command(name, args) if prover.isDefined =>
   1.100 +            prover.get.protocol_command(name, args:_*)
   1.101  
   1.102 -            case change: Session.Change if prover.isDefined =>
   1.103 -              if (global_state.value.is_assigned(change.previous))
   1.104 -                handle_change(change)
   1.105 -              else postponed_changes.store(change)
   1.106 +          case Messages(msgs) =>
   1.107 +            msgs foreach {
   1.108 +              case input: Prover.Input =>
   1.109 +                all_messages.event(input)
   1.110  
   1.111 -            case bad => System.err.println("Session.manager: ignoring bad message " + bad)
   1.112 -          }
   1.113 -          true
   1.114 -          //}}}
   1.115 -        },
   1.116 -      finish = () =>
   1.117 -        {
   1.118 -          if (phase == Session.Ready) {
   1.119 -            _protocol_handlers = _protocol_handlers.stop(prover.get)
   1.120 -            global_state.change(_ => Document.State.init)  // FIXME event bus!?
   1.121 -            phase = Session.Shutdown
   1.122 -            prover.get.terminate
   1.123 -            prover = None
   1.124 -            phase = Session.Inactive
   1.125 -          }
   1.126 -          receiver.cancel()
   1.127 +              case output: Prover.Output =>
   1.128 +                if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
   1.129 +                else handle_output(output)
   1.130 +                if (output.is_syslog) syslog_messages.event(output)
   1.131 +                all_messages.event(output)
   1.132 +            }
   1.133 +
   1.134 +          case change: Session.Change if prover.isDefined =>
   1.135 +            if (global_state.value.is_assigned(change.previous))
   1.136 +              handle_change(change)
   1.137 +            else postponed_changes.store(change)
   1.138 +
   1.139 +          case bad => System.err.println("Session.manager: ignoring bad message " + bad)
   1.140          }
   1.141 -    )
   1.142 +        true
   1.143 +        //}}}
   1.144 +    }
   1.145    }
   1.146  
   1.147  
   1.148 @@ -558,6 +556,8 @@
   1.149  
   1.150    def stop()
   1.151    {
   1.152 +    manager.send_wait(Stop)
   1.153 +    receiver.shutdown()
   1.154      change_parser.shutdown()
   1.155      change_buffer.shutdown()
   1.156      manager.shutdown()