# HG changeset patch # User wenzelm # Date 1452464711 -3600 # Node ID 57895801cb5739a09bbaacff83e10f26490ccfaf # Parent a7cf464933f778844dd50fe7df96b1ae50cdf733 prune old versions more often, to reduce overall heap requirements; diff -r a7cf464933f7 -r 57895801cb57 etc/options --- a/etc/options Sat Jan 09 22:22:17 2016 +0100 +++ b/etc/options Sun Jan 10 23:25:11 2016 +0100 @@ -125,7 +125,7 @@ public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" -public option editor_prune_delay : real = 30.0 +public option editor_prune_delay : real = 15 -- "delay to prune history (delete old versions)" public option editor_update_delay : real = 0.5 diff -r a7cf464933f7 -r 57895801cb57 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sat Jan 09 22:22:17 2016 +0100 +++ b/src/Pure/PIDE/session.scala Sun Jan 10 23:25:11 2016 +0100 @@ -183,7 +183,7 @@ /* tuning parameters */ def output_delay: Time = Time.seconds(0.1) // prover output (markup, common messages) - def prune_delay: Time = Time.seconds(60.0) // prune history (delete old versions) + def prune_delay: Time = Time.seconds(15.0) // prune history (delete old versions) def prune_size: Int = 0 // size of retained history def syslog_limit: Int = 100 def reparse_limit: Int = 0 @@ -353,7 +353,8 @@ /* manager thread */ - private val delay_prune = Standard_Thread.delay_first(prune_delay) { manager.send(Prune_History) } + private val delay_prune = + Standard_Thread.delay_first(prune_delay) { manager.send(Prune_History) } private val manager: Consumer_Thread[Any] = {