src/Pure/PIDE/session.scala
changeset 57866 1dbc506289bb
parent 57842 8e4ae2db1849
child 57867 abae8aff6262
--- 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