# HG changeset patch
# User wenzelm
# Date 1347387723 -7200
# Node ID afcccb9bfa3bd591555df752d8615e4764ce6068
# Parent  ac42d79ab164aa91bed11e83cf84e12e678abff6
prefer tuning parameters as public methods (again) -- to allow overriding in applications;

diff -r ac42d79ab164 -r afcccb9bfa3b src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Sep 11 19:49:17 2012 +0200
+++ b/src/Pure/System/session.scala	Tue Sep 11 20:22:03 2012 +0200
@@ -49,11 +49,10 @@
   /* tuning parameters */
 
   def output_delay: Time = Time.seconds(0.1)  // prover output (markup, common messages)
-
-  private val message_delay = Time.seconds(0.01)  // incoming prover messages
-  private val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
-  private val prune_size = 0  // size of retained history
-  private val syslog_limit = 100
+  def message_delay: Time = Time.seconds(0.01)  // incoming prover messages
+  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
 
 
   /* pervasive event buses */