--- 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
--- 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] =
{