# HG changeset patch
# User wenzelm
# Date 1407261487 -7200
# Node ID 1dbc506289bbbafc41e4883f7593748a78d21823
# Parent  dcfb33c26f50d54de5dd0e946e4860e3b8583087
obsolete (see f7700146678d);

diff -r dcfb33c26f50 -r 1dbc506289bb src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Aug 05 16:58:19 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Aug 05 19:58:07 2014 +0200
@@ -176,7 +176,6 @@
   /* tuning parameters */
 
   def output_delay: Time = Time.seconds(0.1)  // prover output (markup, common messages)
-  def message_delay: Time = Time.seconds(0.1)  // prover input/output 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