author | wenzelm |
Wed, 02 Nov 2022 16:13:29 +0100 | |
changeset 76407 | 7e1a72af970b |
parent 76406 | 40a365360680 |
child 76408 | 2768a6d71570 |
--- a/src/Pure/PIDE/session.scala Wed Nov 02 11:34:24 2022 +0100 +++ b/src/Pure/PIDE/session.scala Wed Nov 02 16:13:29 2022 +0100 @@ -367,7 +367,7 @@ /* manager thread */ - private val delay_prune = + private lazy val delay_prune = Delay.first(prune_delay) { manager.send(Prune_History) } private val manager: Consumer_Thread[Any] = {