author | wenzelm |
Tue, 05 Aug 2014 19:58:07 +0200 | |
changeset 57866 | 1dbc506289bb |
parent 57865 | dcfb33c26f50 |
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