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