obsolete (see f7700146678d);
authorwenzelm
Tue, 05 Aug 2014 19:58:07 +0200
changeset 57866 1dbc506289bb
parent 57865 dcfb33c26f50
child 57867 abae8aff6262
obsolete (see f7700146678d);
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