src/Tools/jEdit/src/syslog_dockable.scala
changeset 56775 59f70b89e5fd
parent 56715 52125652e82a
child 57612 990ffb84489b
     1.1 --- a/src/Tools/jEdit/src/syslog_dockable.scala	Mon Apr 28 15:29:09 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Mon Apr 28 16:17:07 2014 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import scala.swing.TextArea
     1.8 +import scala.swing.{TextArea, ScrollPane}
     1.9  
    1.10  import org.gjt.sp.jedit.View
    1.11  
    1.12 @@ -20,29 +20,24 @@
    1.13  
    1.14    private val syslog = new TextArea()
    1.15  
    1.16 -  private def update_syslog()
    1.17 +  private def syslog_delay = Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay"))
    1.18    {
    1.19 -    Swing_Thread.require {}
    1.20 -
    1.21 -    val text = PIDE.session.current_syslog()
    1.22 +    val text = PIDE.session.syslog_content()
    1.23      if (text != syslog.text) syslog.text = text
    1.24    }
    1.25  
    1.26 -  set_content(syslog)
    1.27 +  set_content(new ScrollPane(syslog))
    1.28  
    1.29  
    1.30    /* main */
    1.31  
    1.32    private val main =
    1.33 -    Session.Consumer[Prover.Output](getClass.getName) {
    1.34 -      case output =>
    1.35 -        if (output.is_syslog) Swing_Thread.later { update_syslog() }
    1.36 -    }
    1.37 +    Session.Consumer[Prover.Output](getClass.getName) { case _ => syslog_delay.invoke() }
    1.38  
    1.39    override def init()
    1.40    {
    1.41      PIDE.session.syslog_messages += main
    1.42 -    update_syslog()
    1.43 +    syslog_delay.invoke()
    1.44    }
    1.45  
    1.46    override def exit()