prune old versions more often, to reduce overall heap requirements;
authorwenzelm
Sun, 10 Jan 2016 23:25:11 +0100
changeset 62115 57895801cb57
parent 62114 a7cf464933f7
child 62116 bc178c0fe1a1
prune old versions more often, to reduce overall heap requirements;
etc/options
src/Pure/PIDE/session.scala
--- 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] =
   {