equal
deleted
inserted
replaced
128 |
128 |
129 |
129 |
130 /* dynamic session options */ |
130 /* dynamic session options */ |
131 |
131 |
132 def output_delay: Time = session_options.seconds("editor_output_delay") |
132 def output_delay: Time = session_options.seconds("editor_output_delay") |
|
133 def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay") |
133 def prune_delay: Time = session_options.seconds("editor_prune_delay") |
134 def prune_delay: Time = session_options.seconds("editor_prune_delay") |
134 def prune_size: Int = session_options.int("editor_prune_size") |
135 def prune_size: Int = session_options.int("editor_prune_size") |
135 def syslog_limit: Int = session_options.int("editor_syslog_limit") |
136 def syslog_limit: Int = session_options.int("editor_syslog_limit") |
136 def reparse_limit: Int = session_options.int("editor_reparse_limit") |
137 def reparse_limit: Int = session_options.int("editor_reparse_limit") |
137 |
138 |
189 private case class Start(start_prover: Prover.Receiver => Prover) |
190 private case class Start(start_prover: Prover.Receiver => Prover) |
190 private case object Stop |
191 private case object Stop |
191 private case class Cancel_Exec(exec_id: Document_ID.Exec) |
192 private case class Cancel_Exec(exec_id: Document_ID.Exec) |
192 private case class Protocol_Command(name: String, args: List[String]) |
193 private case class Protocol_Command(name: String, args: List[String]) |
193 private case class Update_Options(options: Options) |
194 private case class Update_Options(options: Options) |
|
195 private case object Consolidate_Execution |
194 private case object Prune_History |
196 private case object Prune_History |
195 |
197 |
196 |
198 |
197 /* phase */ |
199 /* phase */ |
198 |
200 |
517 protocol_handlers.exit() |
519 protocol_handlers.exit() |
518 global_state.change(_ => Document.State.init) |
520 global_state.change(_ => Document.State.init) |
519 prover.get.terminate |
521 prover.get.terminate |
520 } |
522 } |
521 |
523 |
|
524 case Consolidate_Execution => |
|
525 if (prover.defined) prover.get.consolidate_execution() |
|
526 |
522 case Prune_History => |
527 case Prune_History => |
523 if (prover.defined) { |
528 if (prover.defined) { |
524 val old_versions = global_state.change_result(_.remove_versions(prune_size)) |
529 val old_versions = global_state.change_result(_.remove_versions(prune_size)) |
525 if (old_versions.nonEmpty) prover.get.remove_versions(old_versions) |
530 if (old_versions.nonEmpty) prover.get.remove_versions(old_versions) |
526 } |
531 } |
561 } |
566 } |
562 true |
567 true |
563 //}}} |
568 //}}} |
564 } |
569 } |
565 } |
570 } |
|
571 |
|
572 private val consolidator: Thread = |
|
573 Standard_Thread.fork("Session.consolidator", daemon = true) { |
|
574 try { |
|
575 while (true) { |
|
576 Thread.sleep(consolidate_delay.ms) |
|
577 |
|
578 val state = global_state.value |
|
579 state.stable_tip_version match { |
|
580 case None => |
|
581 case Some(version) => |
|
582 val consolidated = |
|
583 version.nodes.iterator.forall( |
|
584 { case (name, _) => |
|
585 resources.session_base.loaded_theory(name) || |
|
586 state.node_consolidated(version, name) }) |
|
587 if (!consolidated) manager.send(Consolidate_Execution) |
|
588 } |
|
589 } |
|
590 } |
|
591 catch { case Exn.Interrupt() => } |
|
592 } |
566 |
593 |
567 |
594 |
568 /* main operations */ |
595 /* main operations */ |
569 |
596 |
570 def snapshot(name: Document.Node.Name = Document.Node.Name.empty, |
597 def snapshot(name: Document.Node.Name = Document.Node.Name.empty, |
600 send_stop() |
627 send_stop() |
601 prover.await_reset() |
628 prover.await_reset() |
602 |
629 |
603 change_parser.shutdown() |
630 change_parser.shutdown() |
604 change_buffer.shutdown() |
631 change_buffer.shutdown() |
|
632 consolidator.interrupt |
|
633 consolidator.join |
605 manager.shutdown() |
634 manager.shutdown() |
606 dispatcher.shutdown() |
635 dispatcher.shutdown() |
607 |
636 |
608 phase match { |
637 phase match { |
609 case Session.Terminated(result) => result |
638 case Session.Terminated(result) => result |