259 |
259 |
260 private case class Start(name: String, args: List[String]) |
260 private case class Start(name: String, args: List[String]) |
261 private case object Stop |
261 private case object Stop |
262 private case class Cancel_Exec(exec_id: Document_ID.Exec) |
262 private case class Cancel_Exec(exec_id: Document_ID.Exec) |
263 private case class Protocol_Command(name: String, args: List[String]) |
263 private case class Protocol_Command(name: String, args: List[String]) |
264 private case class Messages(msgs: List[Prover.Message]) |
|
265 private case class Update_Options(options: Options) |
264 private case class Update_Options(options: Options) |
266 |
265 |
267 |
266 |
268 /* buffered changes */ |
267 /* buffered changes */ |
269 |
268 |
295 def shutdown() |
294 def shutdown() |
296 { |
295 { |
297 timer.cancel() |
296 timer.cancel() |
298 flush() |
297 flush() |
299 } |
298 } |
300 } |
|
301 |
|
302 |
|
303 /* buffered prover messages */ |
|
304 |
|
305 private object receiver |
|
306 { |
|
307 private var buffer = new mutable.ListBuffer[Prover.Message] |
|
308 |
|
309 private def flush(): Unit = synchronized { |
|
310 if (!buffer.isEmpty) { |
|
311 val msgs = buffer.toList |
|
312 manager.send(Messages(msgs)) |
|
313 buffer = new mutable.ListBuffer[Prover.Message] |
|
314 } |
|
315 } |
|
316 |
|
317 def invoke(msg: Prover.Message): Unit = synchronized { |
|
318 msg match { |
|
319 case _: Prover.Input => |
|
320 buffer += msg |
|
321 case output: Prover.Protocol_Output if output.properties == Markup.Flush => |
|
322 flush() |
|
323 case output: Prover.Output => |
|
324 buffer += msg |
|
325 if (output.is_syslog) |
|
326 syslog.change(queue => |
|
327 { |
|
328 val queue1 = queue.enqueue(output.message) |
|
329 if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1 |
|
330 }) |
|
331 } |
|
332 } |
|
333 |
|
334 private val timer = new Timer("receiver", true) |
|
335 timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms) |
|
336 |
|
337 def shutdown() { timer.cancel(); flush() } |
|
338 } |
299 } |
339 |
300 |
340 |
301 |
341 /* postponed changes */ |
302 /* postponed changes */ |
342 |
303 |
519 Consumer_Thread.fork[Any]("Session.manager", daemon = true) |
480 Consumer_Thread.fork[Any]("Session.manager", daemon = true) |
520 { |
481 { |
521 case arg: Any => |
482 case arg: Any => |
522 //{{{ |
483 //{{{ |
523 arg match { |
484 arg match { |
|
485 case output: Prover.Output => |
|
486 if (output.is_stdout || output.is_stderr) raw_output_messages.post(output) |
|
487 else handle_output(output) |
|
488 if (output.is_syslog) { |
|
489 syslog.change(queue => |
|
490 { |
|
491 val queue1 = queue.enqueue(output.message) |
|
492 if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1 |
|
493 }) |
|
494 syslog_messages.post(output) |
|
495 } |
|
496 all_messages.post(output) |
|
497 |
|
498 case input: Prover.Input => |
|
499 all_messages.post(input) |
|
500 |
524 case Start(name, args) if prover.isEmpty => |
501 case Start(name, args) if prover.isEmpty => |
525 if (phase == Session.Inactive || phase == Session.Failed) { |
502 if (phase == Session.Inactive || phase == Session.Failed) { |
526 phase = Session.Startup |
503 phase = Session.Startup |
527 prover = Some(resources.start_prover(receiver.invoke _, name, args)) |
504 prover = Some(resources.start_prover(manager.send(_), name, args)) |
528 } |
505 } |
529 |
506 |
530 case Stop => |
507 case Stop => |
531 if (prover.isDefined && is_ready) { |
508 if (prover.isDefined && is_ready) { |
532 _protocol_handlers = _protocol_handlers.stop(prover.get) |
509 _protocol_handlers = _protocol_handlers.stop(prover.get) |
553 handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result))) |
530 handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result))) |
554 |
531 |
555 case Protocol_Command(name, args) if prover.isDefined => |
532 case Protocol_Command(name, args) if prover.isDefined => |
556 prover.get.protocol_command(name, args:_*) |
533 prover.get.protocol_command(name, args:_*) |
557 |
534 |
558 case Messages(msgs) => |
|
559 msgs foreach { |
|
560 case input: Prover.Input => |
|
561 all_messages.post(input) |
|
562 |
|
563 case output: Prover.Output => |
|
564 if (output.is_stdout || output.is_stderr) raw_output_messages.post(output) |
|
565 else handle_output(output) |
|
566 if (output.is_syslog) syslog_messages.post(output) |
|
567 all_messages.post(output) |
|
568 } |
|
569 |
|
570 case change: Session.Change if prover.isDefined => |
535 case change: Session.Change if prover.isDefined => |
571 if (global_state.value.is_assigned(change.previous)) |
536 if (global_state.value.is_assigned(change.previous)) |
572 handle_change(change) |
537 handle_change(change) |
573 else postponed_changes.store(change) |
538 else postponed_changes.store(change) |
574 } |
539 } |
584 { manager.send(Start(name, args)) } |
549 { manager.send(Start(name, args)) } |
585 |
550 |
586 def stop() |
551 def stop() |
587 { |
552 { |
588 manager.send_wait(Stop) |
553 manager.send_wait(Stop) |
589 receiver.shutdown() |
|
590 change_parser.shutdown() |
554 change_parser.shutdown() |
591 change_buffer.shutdown() |
555 change_buffer.shutdown() |
592 manager.shutdown() |
556 manager.shutdown() |
593 dispatcher.shutdown() |
557 dispatcher.shutdown() |
594 } |
558 } |