prune old versions more often, to reduce overall heap requirements;
authorwenzelm
Sun Jan 10 23:25:11 2016 +0100 (2016-01-10)
changeset 6211557895801cb57
parent 62114 a7cf464933f7
child 62116 bc178c0fe1a1
prune old versions more often, to reduce overall heap requirements;
etc/options
src/Pure/PIDE/session.scala
     1.1 --- a/etc/options	Sat Jan 09 22:22:17 2016 +0100
     1.2 +++ b/etc/options	Sun Jan 10 23:25:11 2016 +0100
     1.3 @@ -125,7 +125,7 @@
     1.4  public option editor_output_delay : real = 0.1
     1.5    -- "delay for prover output (markup, common messages etc.)"
     1.6  
     1.7 -public option editor_prune_delay : real = 30.0
     1.8 +public option editor_prune_delay : real = 15
     1.9    -- "delay to prune history (delete old versions)"
    1.10  
    1.11  public option editor_update_delay : real = 0.5
     2.1 --- a/src/Pure/PIDE/session.scala	Sat Jan 09 22:22:17 2016 +0100
     2.2 +++ b/src/Pure/PIDE/session.scala	Sun Jan 10 23:25:11 2016 +0100
     2.3 @@ -183,7 +183,7 @@
     2.4    /* tuning parameters */
     2.5  
     2.6    def output_delay: Time = Time.seconds(0.1)  // prover output (markup, common messages)
     2.7 -  def prune_delay: Time = Time.seconds(60.0)  // prune history (delete old versions)
     2.8 +  def prune_delay: Time = Time.seconds(15.0)  // prune history (delete old versions)
     2.9    def prune_size: Int = 0  // size of retained history
    2.10    def syslog_limit: Int = 100
    2.11    def reparse_limit: Int = 0
    2.12 @@ -353,7 +353,8 @@
    2.13  
    2.14    /* manager thread */
    2.15  
    2.16 -  private val delay_prune = Standard_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
    2.17 +  private val delay_prune =
    2.18 +    Standard_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
    2.19  
    2.20    private val manager: Consumer_Thread[Any] =
    2.21    {