added system option editor_output_delay: lower value might help big sessions under low-memory situations;

--- a/etc/options	Tue Aug 05 19:58:07 2014 +0200
+++ b/etc/options	Tue Aug 05 20:40:35 2014 +0200
@@ -117,6 +117,9 @@
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
+public option editor_prune_delay : real = 60.0
+  -- "delay to prune history (delete old versions)"
+
 public option editor_update_delay : real = 0.5
   -- "delay for physical GUI updates"
 

--- a/src/Pure/PIDE/session.scala	Tue Aug 05 19:58:07 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Aug 05 20:40:35 2014 +0200
@@ -176,7 +176,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(60.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

--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 05 19:58:07 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 05 20:40:35 2014 +0200
@@ -391,6 +391,7 @@
 
       PIDE.session = new Session(resources) {
         override def output_delay = PIDE.options.seconds("editor_output_delay")
+        override def prune_delay = PIDE.options.seconds("editor_prune_delay")
         override def reparse_limit = PIDE.options.int("editor_reparse_limit")
       }