added system option editor_output_delay: lower value might help big sessions under low-memory situations;
authorwenzelm
Tue Aug 05 20:40:35 2014 +0200 (2014-08-05)
changeset 57867abae8aff6262
parent 57866 1dbc506289bb
child 57868 0b954ac94827
added system option editor_output_delay: lower value might help big sessions under low-memory situations;
etc/options
src/Pure/PIDE/session.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/etc/options	Tue Aug 05 19:58:07 2014 +0200
     1.2 +++ b/etc/options	Tue Aug 05 20:40:35 2014 +0200
     1.3 @@ -117,6 +117,9 @@
     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 = 60.0
     1.8 +  -- "delay to prune history (delete old versions)"
     1.9 +
    1.10  public option editor_update_delay : real = 0.5
    1.11    -- "delay for physical GUI updates"
    1.12  
     2.1 --- a/src/Pure/PIDE/session.scala	Tue Aug 05 19:58:07 2014 +0200
     2.2 +++ b/src/Pure/PIDE/session.scala	Tue Aug 05 20:40:35 2014 +0200
     2.3 @@ -176,7 +176,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(60.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
     3.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 05 19:58:07 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 05 20:40:35 2014 +0200
     3.3 @@ -391,6 +391,7 @@
     3.4  
     3.5        PIDE.session = new Session(resources) {
     3.6          override def output_delay = PIDE.options.seconds("editor_output_delay")
     3.7 +        override def prune_delay = PIDE.options.seconds("editor_prune_delay")
     3.8          override def reparse_limit = PIDE.options.int("editor_reparse_limit")
     3.9        }
    3.10